Erdős problem 70

Erdős Problem 70: Let

\mathfrak{c}

be the order type of the real numbers, let

\beta

be a countable ordinal, and let

2 \le n < \omega

. Is it true that

\mathfrak{c} \to (\beta, n)^3_2

? Note: The cases

n \le 3

are trivially true (compare omega_three), so the genuine content of the conjecture begins at

n = 4

$1,024 bounty

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Where this lives

conjectures-tasks

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

versions/fc-v2-erdos70-erdos-70-ff0f40a80b3ae01d61c3f712-formalized →

Formal statement

Proof target

import Mathlib
import FormalConjectures.ErdosProblems.«70»
import TaskSupport

namespace Bounty

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

end Bounty

Open this target’s Challenge.lean Task bundle on GitHub

Original conjecture (Lean type)

∀ (β : Ordinal.{0}) (n : ℕ), β.card ≤ Cardinal.aleph0 → 2 ≤ n → Erdos70.RealCardinalRamsey3 β ↑n

Original conjecture source: FormalConjectures/ErdosProblems/70.lean

The audit patch changes this file, so the upstream version can differ from the statement above.

Source type SHA-256: sha256:53899d90ff42ae9c872fb045beaa22838d344ed2562f785dafda2ac81938367c
Task id: fc-v2-erdos70-erdos-70-ff0f40a80b3ae01d61c3f712-formalized
Task commitment: sha256:90cb390366b084f850a7f0db307231eb8f532f7b3f230e897b7ae49b63892cc5

References

erdosproblems.com/70

[ErRa56] Erdős, P. and Rado, R., A partition calculus in set theory, Bull. Amer. Math. Soc. 62 (1956), 427–489, Theorem 31.
[Er87] Erdős, P., Some problems on finite and infinite graphs, Logic and combinatorics (Arcata, Calif., 1985), Contemp. Math. 65 (1987), 223–228.

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.

Bittensor Discord