Proof Ledger: public review status for the AI proof flood

The Erdős-problem corner of this idea is already covered. erdosproblems.com, Tao's GitHub wiki and dashboards built on their data track AI claims together with Lean status, and mathematicians already trust them. A new entrant cannot win there. What I did not find is a neutral ledger that covers every AI-claimed math result across labs and problem sources. That would include OpenAI's ten-result package, Anthropic's FLT formalization, DeepMind and AlphaProof claims, and one-off results posted on X or arXiv. The ledger would record more than "Lean-checked". It would record whether the formal statement actually matches the claimed theorem, who did the human review, and which errors are known. That gap between the formal statement and the intended meaning is exactly what the OpenAI audit paper and press coverage flag as missing. The closest thing to it, Kingy.ai's tracker, is run by a media site, not by mathematicians, so a ledger run by mathematicians and edited through pull requests could still earn more credibility. On the bounty side I found no dedicated per-result formalization bounty board. Funding goes out as grants (Renaissance Philanthropy, XTX, Microsoft Research) or one-off crowdfunding (Manifund). The risks are that AI labs now formalize their own results before release, which shrinks the bounty market, and that the obvious sponsors may simply fund erdosproblems.com or the Mathlib Initiative directly. A credible way in is to partner with Bloom and Tao rather than compete with them, and to focus on statement-fidelity review, which labs cannot credibly certify themselves.

• Terence Tao's AI contributions to Erdős problems wiki (erdosproblems GitHub repo)

  This is a community wiki, edited on GitHub, that logs AI contributions to Erdős problems. It is very close to the Proof Ledger idea, but it only covers Erdős problems. One source says it stopped being updated after 2026-06-30, which I could not confirm.

• erdosproblems.com (Thomas Bloom)

  Each problem page carries a status such as PROVED (LEAN), and forum threads hold the review discussion and Lean links. In practice it is already the main verification record for AI claims on Erdős problems.

• Jason Willems Erdős Problems Database visualization

  This dashboard is built on the Bloom/Tao data. It counts problems with Lean-formalized proofs and disproofs (a snapshot dated 2026-09-09 shows 176 Lean-formalized proofs). It shows there is demand, and that people will build free trackers without a sponsor.

• Kingy.ai Breakthrough Tracker

  Each record covers one AI-linked math result and carries labels like 'Provisional, Lean-checked claim, specialist review pending'. That is almost exactly the Proof Ledger field set. It is run by an AI-news media site, not by mathematicians.

• A Human Audit of OpenAI's AI-Generated Mathematical Proofs (arXiv)

  This is a one-off audit paper on OpenAI's August 2026 package of ten Lean-certified results. It points out that a Lean certificate only covers the statement as encoded, so humans still have to check the meaning. That matches the ledger's premise, but it is a paper, not a maintained tracker.

• Renaissance Philanthropy AI for Math Fund / Mathlib Initiative

  This is the sponsor-funded model the bounty board would compete with or sell to. XTX Markets money backs Lean and formalization work through grants, not per-theorem bounties. It is a likely customer or partner rather than a direct competitor.

• Manifund project: formalizing mathematical AI safety research in Lean

  Crowdfunding for Lean formalization does exist on general platforms like Manifund. I found no marketplace dedicated to per-result formalization bounties.

Checked 2026-10-11