Lean formalization workspace for selected problems.
- Problem statements are stored as Markdown files at
Firstproof/Problem*/proofdocs/problem.md. - Only Problem 9 is solved.
- Toolchain is pinned to Lean v4.22.0 (
lean-toolchain), and the Problem 9 proof is compatible with Lean v4.24. - Problems 4 and 6 are formalized/copied from the DeepMind
formal-conjecturesproject. - Problem 9 was autonomously solved informally and then agentically proven in Lean.