Logic and foundations
Withdrawnerdos_rado), which covers all red ordinals below .
This variant asks whether the result extends to , 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.)
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
Original conjecture (Lean type)
True ↔ Erdos70.OrdinalCardinalRamsey3 Cardinal.continuum.ord (Ordinal.omega0 * 2) 4Original conjecture source: FormalConjectures/ErdosProblems/70.lean
References
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.