Erdős problem 70 - omega times two four

**First open case beyond Erdős–Rado**:

\mathfrak{c} \to (\omega \cdot 2, 4)^3_2

. Erdős and Rado proved

\mathfrak{c} \to (\omega + n, 4)^3_2

for every finite

n \ge 2

(see erdos_rado), which covers all red ordinals below

\omega \cdot 2 = \omega + \omega

. This variant asks whether the result extends to

\beta = \omega \cdot 2

, the simplest countable ordinal not covered by their theorem.

Withdrawn 6 Oct 2026

SOLVED_EXTERNALLY (Milner and Prikry (1991) prove in ZFC the stronger relation omega_1 -> (omega*2+1, 4)^3; restricting to an initial omega_1 segment of the continuum ordinal gives this exact well-ordered variant. Only this variant is retired: the general Erdős 70 question, the real-line order question and the other Erdős 70 statements are unaffected. conjectures.io result 81f38614-217d-4eef-aadf-d3fd9d62a8d0 already recorded NOT_NOVEL for this variant. This retirement did not independently rebuild a proof. See EXTERNAL-SOLUTIONS-2026-10-06.md.)

1 proof submitted, 17 days ago

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«70»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos70.erdos_70.variants.omega_times_two_four" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔ Erdos70.OrdinalCardinalRamsey3 Cardinal.continuum.ord (Ordinal.omega0 * 2) 4

Original conjecture source: FormalConjectures/ErdosProblems/70.lean

Task id: fc-6a786f99-variants-omega-times-two-four-4eb41de4f8-formalized-v1
Task commitment: sha256:89a9664a7e355009a693117c51eaac8223b8d2004bfa49127244df10fa7c6dbb

References

erdosproblems.com/70

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord

Contribution history

Individual lemmas, special cases and supporting work, shown in their original scope.

Nothing has been published against this problem yet.

Where this lives

conjectures-tasks

The pinned statement, the Lean challenge file and the exact bundle you build against.

pool/tier-1/erdos-70-variants-omega-times-two-four-formalized →

conjectures-contribution

Every published piece for this problem, with its Lean source and its signed record.

contributions/erdos-70-variants-omega-times-two-four →