Palomar opens a Lean proof registry for the AI math pileup

Palomar, a public registry for Lean-verified mathematics, opened for submissions on August 18, offering fixed GitHub snapshots, mechanical proof checks, and LLM-based semantic review. UCLA mathematician and 2006 Fields Medalist Terence Tao announced the launch, positioning the project as a response to the proliferation of AI-generated proofs. Palomar is maintained by Tao, Matthew Ballard, Nestor Guillen, and Jaume de Dios Pont, and was incubated by the Lean Focused Research Organization and the Institute for Computer-Aided Reasoning in Mathematics.

Palomar opens a Lean proof registry for the AI math pileup The project registers fixed GitHub snapshots, checks Lean proofs mechanically, and uses an LLM to compare formal statements with informal descriptions. By RuntimeWire Staff /author/runtimewire-staff · Published Primary source: Terence Tao https://terrytao.wordpress.com/2026/08/18/palomar-a-registry-of-lean-verified-mathematics/ Why it matters Palomar gives Lean proofs fixed, commit-level records and separates mechanical verification from semantic LLM review. Its narrow scope provides researchers with an audit trail while explicitly stopping short of peer review. Palomar https://palomar-registry.org/?ref=runtimewire opened for submissions on August 18, giving mathematicians a public registry where formal proofs written in Lean can be tied to fixed source code, mechanically checked, and inspected after the initial announcement has moved on. Terence Tao https://math.ucla.edu/~tao/preprints/cv.html?ref=runtimewire , the UCLA mathematician and 2006 Fields Medalist, announced the opening in a blog post https://terrytao.wordpress.com/2026/08/18/palomar-a-registry-of-lean-verified-mathematics/?ref=runtimewire . Tao is one of Palomar's four initial technical maintainers, alongside Matthew Ballard https://sc.edu/study/colleges schools/artsandsciences/mathematics/our people/directory/ballard matthew.php?ref=runtimewire , Nestor Guillen https://www.ndguillen.com/about.html?ref=runtimewire , and Jaume de Dios Pont https://jaume.dedios.cat/?ref=runtimewire . The project was incubated by the Lean Focused Research Organization https://lean-lang.org/fro/?ref=runtimewire and the Institute for Computer-Aided Reasoning in Mathematics https://icarm.io/?ref=runtimewire ICARM . Tao framed the project as a response to a proliferation of AI-generated proofs, including some formalized in Lean. He wrote that checking those repositories remains difficult for readers without Lean expertise: the proof must typecheck, avoid unauthorized axioms, and formally state the same result described in ordinary mathematical language. Palomar's answer is a registry record of what a fixed repository snapshot proves. Tao described it as a "zeroth approximation" of a preprint server for Lean proofs. The comparison sets the right expectation. Palomar creates an indexable artifact and an audit trail. It does not referee the mathematics. Tao's role gives the effort visibility, though Palomar's operating structure is distributed. Ballard is a University of South Carolina algebraic geometer. Guillen works in partial differential equations, the calculus of variations, and scientific computing. De Dios Pont, who completed his UCLA doctorate under Tao in 2023, is an NYU Center for Data Science faculty fellow working on AI for mathematics alongside harmonic analysis and spectral theory. The wider scientific advisory board includes Jeremy Avigad, Bryna Kra, Kim Morrison, Ravi Vakil, and Akshay Venkatesh. What Palomar actually checks Tao's launch post https://terrytao.wordpress.com/2026/08/18/palomar-a-registry-of-lean-verified-mathematics/?ref=runtimewire describes Palomar as a registry of external GitHub repository snapshots represented by specific commits. Each submission includes a short Challenge.lean file stating the claimed result, a Solution.lean module containing the proof, and a formalization.yaml https://github.com/mathlib-initiative/formalization.yaml?ref=runtimewire file with an informal description, metadata, and disclosures. The mechanical check uses Comparator https://github.com/leanprover/comparator?ref=runtimewire , a Lean tool that separates the advertised statement from its proof and checks whether the solution establishes the result in the challenge file. Lean's documentation https://lean-lang.org/doc/reference/latest/ValidatingProofs/?ref=runtimewire says Comparator supports theorem-statement matching and can use Lean's kernel and the independently implemented Nanoda checker. The available materials do not establish that Palomar requires every Comparator validation option. That separation addresses a subtle failure mode. A repository can contain a valid proof while its formal statement differs from the theorem described outside the code. Keeping the challenge statement apart from the solution gives readers a smaller surface to inspect. Palomar's second check is nondeterministic. According to Tao's announcement, a large language model evaluates whether the informal description in formalization.yaml appears to match the formal result and whether the repository meets the registry's minimum standards. Palomar's published policy https://github.com/PalomarRegistry/PalomarPolicy?ref=runtimewire describes an automated registration review, while the supplied materials do not establish whether maintainers conduct separate human moderation. Tao also recommends human review during submission and says Palomar's checks fall well short of peer review for novelty, interest, and accuracy. The registry therefore combines mechanical proof checking with a model-based assessment of the semantic bridge between Lean code and ordinary mathematical language. The project documentation https://palomar-registry.org/about?ref=runtimewire warns that language-model review can miss discrepancies. Readers still have to examine whether the definitions and formal statement capture the theorem being discussed. Verification without an endorsement Palomar draws firm boundaries around its claims. Registration does not certify novelty, importance, code quality, or the correctness of an informal proof. It does not mean an expert referee has reviewed the work, and it does not turn a GitHub repository into a journal publication. The useful claim is narrow: a proof from a specified repository snapshot passed Palomar's documented mechanical and automated checks. The challenge file, solution, and accompanying account then give other researchers material they can inspect and challenge. That distinction matters as AI-assisted formalization spreads. A proof checker can determine whether code establishes a formal statement under its encoded assumptions. A public mathematical claim also depends on whether that statement, its definitions, and its informal description refer to the same result. Tao and the Palomar maintainers are building infrastructure for that second layer while keeping the registry's claims deliberately limited. Palomar currently supports Lean, and submissions may be human-generated, AI-generated, or produced through a mixture of both. Palomar will not settle arguments about machine-generated mathematics. It gives those arguments fixed repository snapshots and explicit claims to examine, which is useful infrastructure in a field already contending with a proliferation of automated proofs.