This repository contains artifacts generated by AxiomProver related to the Erdős problems, listed on Thomas Bloom's website.
| Problem | Lean formalization |
|---|---|
| 209 | solution.lean |
| 231 | solution.lean |
| 276 | solution.lean1 |
| 328 | solution.lean |
| 403 | solution.lean |
| 441 | solution.lean |
| 1134 | solution.lean |
This repository uses the MIT License. See LICENSE for details.
Footnotes
-
This formalization is for the literal problem statement, e.g., as stated in Google DeepMind. This means it merely formalizes the covering system solution from Graham. ↩