Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
AI agents wired into Lean 4 and large-scale cloud compute are now generating machine-checked proofs for dozens of hard Erdős problems, raising both excitement and unease about what this means for mathematical research. Commenters probe the technical setup, funding, and open-sourcing plans, and note that while the formal proofs are compelling, turning them into human-readable, insightful arguments remains a separate challenge. The exchange broadens into questions about the value of “useless” pure math, the future role of human mathematicians as proof search automates, and how AI-driven theorem proving might eventually tie into real-world impact and economic change.
Infrastructure, Compute, and Model Access
- Project uses many Codex accounts via OAuth tokens and a custom broker that load-balances API calls; “running GPT locally” was a wording issue, not self-hosting the model.
- Local compute is a multi‑vCPU server; commenters note such hardware is affordable for hobbyists.
- AI agents have bash tools and access to preinstalled math packages on VMs.
- Models mentioned: GPT‑5.6 (for generation), Fable (for Lean proof checking/summaries), Gemini embeddings.
Harness, Open Sourcing, and Contributions
- Questions focus on the “agentic harness”: how loops are orchestrated, which models “drive,” and how progress is measured; details remain high-level.
- Another participant describes a similar independent system: sovereign inference on intranet, sandboxed workers for Lean/Sage, open-weight models, and plans for further fine-tuning.
- There is interest in open-sourcing the system and enabling contributions; the author says the project began as a quick, self-contained experiment and may be opened up later.
Validity, Rigor, and Writeups
- Lean 4 proofs are machine-checked; Fable serves as a kind of referee.
- Criticism: proof summaries are technically dense and poorly tailored to human readers; transforming formal proofs into clear, aesthetic explanations is a distinct, still-missing step.
- Author acknowledges this and plans to improve writeups.
- Some submitted Erdős solutions were temporarily withdrawn not for incorrectness but for confusing framing or being only partial; work is ongoing.
- Suggestion to integrate Lean’s “comparator” tool to guard against subtle unsoundness when modifying contexts.
Value of Pure Math and AI Theorem Proving
- Debate over whether “useless” pure math is self-contained and socially unimportant versus its history of unexpected applications (e.g., cryptography) and intrinsic aesthetic value.
- Some see solving Erdős problems as a benchmark and source of techniques rather than direct applications; real-world impact may come more from frontier or Millennium problems.
- Others argue that, even if purely recreational, this is as legitimate as any intellectual hobby.
Impact on Mathematicians and Society
- Concerns that AI proof systems might “suck the fun out of math” and threaten mathematicians’ jobs; pushback likens this to earlier automation fears (e.g., looms, calculators).
- Several argue mathematicians will shift toward understanding, conjecturing, and vetting AI-generated proofs; advanced proofs are already often beyond a single human’s capacity.
- Broader thread on decoupling livelihood from work, potential UBI, and taxing AI firms; disagreement on how urgent policy changes are.
State and Future of AI in Mathematics
- Many express amazement that LLMs can now solve nontrivial Erdős problems; perception is shifting from “can LLMs do math?” to “how far can we push this?”
- Anticipated future: massive autoformalization of existing math, large‑scale automated conjecture generation and evaluation, and possibly distributed, BOINC‑style efforts for mathematical exploration.