Palomar Registry Puts AI Math Proofs Under Lean Review

Terence Tao announced on August 18, 2026 that Palomar is open for submissions. Incubated by the Lean FRO and by ICARM, Palomar is a registry of Lean-verified mathematics, and Tao describes it as the analogue of a preprint server for formal proofs. The timing is not incidental. AI systems have been producing formalized proofs at a pace that outstrips anyone's ability to eyeball them, and a registry is the infrastructure that turns a pile of repositories into something a mathematician can actually cite.

• Palomar registers external GitHub repositories containing Lean code that follows current formalization best practices
• Each submission needs a challenge file stating the claimed result in short, human-readable Lean, plus a solution module containing the proof
• A formalization metadata file carries informal descriptions, relevant metadata, and disclosures about how the work was produced
• The registry checks that a repository proves what it claims and that the proof does not lean on extra axioms or other shortcuts

Why Does a Lean Proof Registry Exist Now?

Lean's appeal has always been that a proof either compiles or it does not. That property becomes much more valuable, and much more load-bearing, when proofs start arriving faster than humans can read them. Over recent months the volume of AI-generated formalizations has climbed sharply, and with it a practical problem: a repository can compile cleanly and still not prove the theorem its summary advertises.

The failure modes are mundane rather than dramatic. A statement can be formalized in a way that is technically true but weaker than the informal claim. A proof can quietly introduce an additional axiom that makes the result unremarkable. A file can prove a special case while the description covers the general one. None of these require bad intent, and all of them are hard to spot without structured review.

Palomar's answer is structure. The challenge file forces the claim into a short, readable form separate from the proof. The solution module can be arbitrarily long, because nobody needs to read it. The metadata file records what was claimed, in ordinary language, alongside disclosures about how the work was produced.

How Palomar Differs From Publishing a Proof Yourself

The distinction matters. Anyone can push Lean code to a public repository, and plenty of people do. What a registry adds is a fixed source version, a verification run against that version, and a published record of exactly which statements were checked, which library dependencies they rest on, and what reviewers observed. That is the difference between a link and a citation.

It also creates a shared reference point for a field that has been improvising. We have covered several rounds of AI-assisted formal mathematics, including OpenAI's Astra proving ten open problems in Lean 4 and the open-source Leanstral 1.5 theorem-proving model. Each of those raised the same follow-up question from readers: how would I check any of this? Palomar is a serious attempt at an answer.

What This Means for AI-Assisted Mathematics

The optimistic reading, and the one the project seems to hold, is that verification infrastructure is what lets AI contribution scale without eroding trust. If a claimed result carries a machine-checked statement, a dependency list, and an honest disclosure of how it was produced, the provenance question stops being adversarial. Reviewers can spend their attention on whether a result is interesting rather than on whether it is real.

Named after the observatory, Palomar is starting small and open. For mathematicians and engineers curious about where machine-checked proof is heading, it is worth watching what accumulates there over the next few months, and how many submissions disclose substantial AI involvement.

More on formal methods and research tooling in our artificial intelligence coverage.

Sources: What's new, Terence Tao — August 18, 2026; Palomar Registry — August 2026.