Palomar: A Registry for Lean-Verified Mathematics Opens for Submissions

Palomar: A registry of Lean verified mathematics

Terence Tao announces the launch of Palomar, a registry for Lean-verified mathematics, incubated by Lean FRO and ICARM. It accepts external GitHub repositories containing Lean code that proves specific results, with automated checks to ensure proofs typecheck and informal descriptions match. The registry aims to bring clarity to the growing number of AI-generated proofs, though it is not a peer-reviewed journal. Tao serves on its scientific advisory board and has already submitted his formalization of Sendov's conjecture.