A collection of Lean proofs for problems from erdosproblems.com.
Each proof is self-contained. Every ErdosN.lean file's only import is import Mathlib, with no cross-references to other files in the repository. Additionally, some proofs depend on extra axioms declared in the proof itself, or on mechanisms that expand Lean's trusted base. The table below shows the state of each problem and any axioms or trust extensions it relies on (state definitions live in schema/problems.schema.json). Original sources are recorded in the sources field of data/problems.yaml.
For problem N, problems/N/ contains:
ErdosN.lean: the prooflakefile.toml: packageerdosN, Mathlib revision, libraryErdosNlean-toolchain: the Lean versionlake-manifest.json: dependency lockfile
Verify with:
cd problems/N
lake exe cache get
lake build199 proofs in the catalog (out of 199 Erdős problems with formalized solutions):
- 182
complete - 3
trust_extended - 14
axiomatic