Tagewerk VII
Erdős problems — first batch: faithful Lean statements (Straus, Ginzburg–Ziv, Szekeres, Turán)
The Erdős statement-formalization lane, applied to a first operator-picked batch. The Erdős database is dominated by asymptotic problems the kernel cannot decide, so the contribution is faithful Lean STATEMENTS (not solutions), each passing a faithfulness gate: the conjecture Prop elaborates, a faithfulness anchor holds, and a non-vacuity note records the load-bearing quantifier structure. Erdős–Straus (open): for every n ≥ 2, 4/n is a sum of three unit fractions — anchored by the concrete 4/5 = 1/2 + 1/4 + 1/20. Erdős–Ginzburg–Ziv (theorem, 1961): among any 2n−1 integers some n have a sum divisible by n. Erdős–Szekeres (theorem, 1935): an injective real sequence longer than r·s has a strictly-monotone subsequence of length > r or > s — here the statement is PROVED, being exactly Mathlib's `erdos_szekeres`. Erdős–Turán on APs (open, 1936): if the reciprocals of a set of positive integers diverge, the set contains arbitrarily long arithmetic progressions. Statements are sourced from the mathematical literature, not scraped from erdosproblems.com (their AI-contribution policy is respected). Each file downloads verbatim (verify the SHA-256) and re-verifies against Lean 4.31 + Mathlib.
Verdicts — machine-adjudicated (4)
- FORMALIZED Straus Erdős–Straus: 4/n as a sum of three unit fractions
OPEN. ∀ n≥2 ∃ a,b,c>0 with 4/n = 1/a+1/b+1/c. Faithfulness anchor: the concrete decomposition 4/5 = 1/2+1/4+1/20 (kernel-checked).
- FORMALIZED EGZ Erdős–Ginzburg–Ziv: n of any 2n−1 integers sum to 0 mod n
Theorem (1961). Anchor: the n=1 instance elaborates. The card=n and divisibility clauses are the content.
- PROVED Szekeres Erdős–Szekeres: monotone subsequences
Theorem (1935). The formal statement is exactly Mathlib's `erdos_szekeres` — so it is not merely stated but kernel-PROVED (erdos_szekeres_proof).
- FORMALIZED Turán Erdős–Turán: divergent reciprocals ⟹ arbitrarily long APs
OPEN (primes case = Green–Tao). ¬Summable(1/a) → ∀k ∃ length-k AP ⊆ A. Anchor: the AP-in-a-set clause on {0,2,4}.
Re-runnable artifacts
- erdos_straus.lean ↓ sha256 592dae94a3b4…
- erdos_ginzburg_ziv.lean ↓ sha256 cb80ea834578…
- erdos_szekeres.lean ↓ sha256 55865c9f69b1…
- erdos_turan_ap.lean ↓ sha256 46c91107b77a…
Files download verbatim from this site — the exact kernel-checked bytes (verify the SHA-256). See how to re-verify.
Repositories — the code trail
- produced elementalcollision/leibniz-daemon #285 scripts/erdos_formalize.py + docs/erdos/erdos_{straus,ginzburg_ziv,szekeres,turan_ap}.lean
References
- Erdős, P., & Straus, E. G. (c. 1948). The Erdős–Straus conjecture: for n ≥ 2, 4/n = 1/x + 1/y + 1/z in positive integers. [Folklore conjecture.]
- Erdős, P., Ginzburg, A., & Ziv, A. (1961). Theorem in the additive number theory. Bulletin of the Research Council of Israel, 10F, 41–43.
- Erdős, P., & Szekeres, G. (1935). A combinatorial problem in geometry. Compositio Mathematica, 2, 463–470.
- Erdős, P., & Turán, P. (1936). On some sequences of integers. Journal of the London Mathematical Society, 11(4), 261–264.