Palomar launches: a registry of Lean-verified mathematics to curb misrepresented AI proof claims
On 18 Aug 2026 the Lean FRO and ICARM launched Palomar (palomar-registry.org), "the analogue of a preprint server for Lean proofs". It indexes GitHub repositories whose formal results are checked mechanically with Lean's Comparator tool and checked with an LLM for semantic alignment with the informal statement. It was built in response to the flood of AI-generated proofs, and explicitly does not claim peer-review status.
Key facts
- Each entry: a human-readable challenge file, a solution module with the formal proof, and a formalization.yaml with informal description and metadata
- Automated checks: mechanical verification via leanprover/comparator plus LLM-based semantic-alignment check
- Scientific advisory board incl. Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Terence Tao, Ravi Vakil, Akshay Venkatesh
- First entry PALOMAR-2026-08-13-000001 (teorth/sendov, the Sendov conjecture formalisation)
- Aim: minimal safeguard against misrepresentation of AI claims, not a judgement of novelty or significance
Science result
- Field
- mathematics / formal verification / research infrastructure
- Problem
- Trustworthy registration of (often AI-generated) formal proofs
- Result
- Public registry of Lean-verified results with automated formal and semantic checks.
- AI system
- n/a
- Human role
- Human-built infrastructure; uses an LLM for semantic-alignment checks
- Verification
- Lean Comparator + LLM alignment check
- Status
- confirmed
What happened
As AI systems produced Lean proofs of old and new results at a growing rate, the Lean community set up a registry that makes formal claims inspectable and checks mechanically that a formal statement matches what is claimed informally.
Why it matters
Formal verification became the main way to trust AI mathematics in 2026. Palomar supplies the missing public infrastructure: a place where "proved in Lean" can be checked rather than asserted.
Changelog
- 2026-09-29: created (lead from data/leads.md)
Related events
- Sendov's 1958 conjecture on polynomial roots proved with GPT-5.6 Pro; Tao simplifies and formalises it ★★★★
- SAIR launches the Open Math Model initiative for community-governed open-weight math AI, plus Lean Kernel and Andrews–Curtis challenges ★★★
- Terence Tao's ICM 2026 public lecture 'Mathematics in the age of AI' calls a crisis in the foundations of mathematical values ★★★
Sources (5)
- officialPalomar registry
- officialTerence Tao: Palomar, a registry of Lean-verified mathematics
- officialPalomar statement
- codeGitHub: leanprover/comparator
- codeGitHub: mathlib-initiative/formalization.yaml
id: 2026-08-18-palomar-lean-registry · updated 2026-09-29 · open in the interactive timeline