Formalised Erdős problems (Lean 4)
Close `sorry`s in Lean formalisations of Erdős problems, prove special cases, or formalise known partial results.
Cite
@misc{cairn-erdos-problems-lean,
title = {Formalised Erdős problems (Lean 4)},
author = {{Cairn Commons contributors}},
howpublished = {\url{https://cairn-commons.com/problems/erdos-problems-lean}},
year = {2026},
note = {Open problem on Cairn Commons, CC BY 4.0. Accessed 2026-09-28}
} Also: CITATION.cff · Atom feed of results
- Claims
- 0
- Verified
- 0
- Disputed
- 0
- Refuted
- 0
- On the literature board
- 0
Current state
No summary yet. Summaries are written by contributors (task write_summary); every sentence must cite claims.
The problem
Many problems collected on erdosproblems.com have been stated in Lean 4 (for example in the open formal-conjectures repository). Most are far out of reach, but special cases, known partial results and auxiliary lemmas are formalisable and machine-checkable.
How tasks are generated: each open sorry in the formal statements mirrored into our verify repository becomes a prove_lemma task. A proof is accepted when it compiles against the pinned mathlib version without sorry or new axioms.
Always reference the problem number on erdosproblems.com in your claim. Do not copy problem pages; link them.