Palomar: a registry of Lean-verified mathematics.
Since the start of 2026, the volume and complexity of machine-assisted proofs and machine-assisted formalizations have risen substantially.
Formalization consists of translating mathematical statements (as they appear in research journals and books) into a rigorous symbolic language, such as Lean, Rocq, or Isabelle. Formalized proofs can then be mechanically verified, to check that every logical step follows from the stated assumptions. Formalizing mathematics has advantages beyond the verification of logical soundness: it can also influence how we approach a problem or complex theory. More recently, a different use of Lean formalization has emerged: as a “check” on the (non-deterministic) output of mathematical arguments by a Large Language Model, filtering out faulty logic, and, as a result, speeding up the exploration of valid mathematical arguments.
These are powerful new tools now at the disposal of mathematicians; they can help us explore and interact with our vast mathematical heritage, and to meaningfully add to it.
These new tools, however, also present us with serious challenges. Bold claims about machine-assisted resolution of famous problems are being announced every day with poor vetting, insufficient transparency, and inadequate context. The volume of such announcements is increasing rapidly. This situation is generating confusion, while also eroding our current standard for what constitutes an “established mathematical fact”.
We are caught between the growing importance of machine-assisted and machine-generated mathematics on one side, and the emergence of many unvetted claims. Press releases, social media posts, and company websites are insufficient mechanisms for documenting a mathematical formalization. These rapid changes make it imperative that we establish community-accepted minimum standards for what constitutes, in the era of machine-generated proofs, a baseline contribution to mathematics. We should build automatic tools to verify adherence to such standards, to the extent possible.
With this in mind, we are establishing the Palomar Registry, a new public registry of Lean-verified mathematics.
Palomar, named after the Palomar Observatory Sky Survey, is a searchable registry of Lean formalizations that have met certain requirements. The role of the registry in the research publishing pipeline is similar to that of a repository or preprint server: it provides a durable, indexable record of formalizations of results of interest to the mathematical research community. As is the case with repositories like arXiv, the appearance of a work in the registry does not constitute a certificate of novelty, nor a certification of relevance, nor a certification that the verified statement matches the informal statement.
Palomar uses three key technologies from the Lean ecosystem to create a reliable, valuable record.
- Every submission must use the comparator technology developed by the Lean FRO, which ensures a clean separation of the statement of the theorem and its proof, allowing readers of the Palomar record to know exactly what they need to audit (the statement), and what is being ensured by Lean. Further, comparator allows Palomar to securely check the proof (even in the face of adversarial Lean proofs).
- Every submission must have a formalization.yaml file. This is a recent standard developed by the Mathlib Initiative, which provides a standard structure for describing the provenance and status of a formal proof. There are fields for recording collaborations (in particular with authors of an original informal proof), for recording any use of AI (including models and budgets), and for reporting adherence to social standards (e.g. around licensing, referencing, and attribution).
- Palomar automatically uses Verso, the new documentation preparation system developed by the Lean FRO, to render the main claimed formal theorem into the web page, with inline hover information explaining the meaning of Lean terms.
The Palomar documentation explains how to prepare submissions compatible with these tools, and LLMs can effectively assist. Other proof assistants may be added to Palomar later. We believe the use of each of these tools is essential good practice in all serious formalization efforts, and we hope that Palomar insisting on them will help raise standards for everyone.
It is our hope that the registry will serve as useful infrastructure for traditional journals. As with arXiv overlay journals, a journal looking to incorporate Lean formalizations into its editorial work is welcome to have authors submit their formalizations to Palomar. On the other hand, formalization can serve as an important guarantor of mechanical correctness. By firmly establishing a minimum standard for verification, Palomar frees traditional journals to aim higher—allowing referees to focus their scarce time on conceptual novelty and elegance, rather than grinding through baseline logic.
The mathematical community must retain its central role in setting standards, rather than have them emerge de facto in the wild or be imposed by external parties with values in conflict with the advancement of mathematics. This is a matter of importance to every mathematician, including those who are not currently using these technologies.
We see the Palomar Registry as one of many needed pieces of institutional infrastructure to support the values and priorities of mathematicians as new technologies become more widely adopted. While no single person or subset can speak for all mathematics, we hope this project encourages other mathematicians to propose similar initiatives.
At present, the Palomar registry is jointly incubated by ICARM and the Lean Focused Research Organization, and the initial Scientific Board consists of the undersigned authors. This is only a preliminary governance structure, making use of the available interest and resources. We anticipate it will evolve according to the community’s needs, and we commit to working with and for the mathematical research community.
Jeremy Avigad, Matthew Ballard, Jaume De Dios, Nestor Guillen, Bryna Kra,
Kim Morrison, Terence Tao, Ravi Vakil, and Akshay Venkatesh.