This repository contains a formal Lean proof of OpenAI's 2026 counterexample to the Erdős unit distance conjecture. See this Leanprover Zulip thread for more information.
At the moment, the repository contains two directories:
src/original/ is the original proof from the model, while
src/submission/ is (essentially) the submission provided to
lean-eval.