Palomar - a registry of Lean-verified mathematics

Palomar, a new public registry of machine-checked mathematical results formalized in Lean, launched in August 2026. Initially incubated by Lean FRO and ICARM, Palomar provides a searchable and durable record of formalizations, including the exact statements checked,

Matthew Ballard serves as one of Palomar’s four initial Technical Maintainers and as an initial Moderator and member of its Scientific Advisory Board. More details are on the about page.