Palomar launches: a registry of Lean-verified mathematics to curb misrepresented AI proof claims
Result confirmed
The takeaway
On 18 Aug 2026 the Lean FRO and ICARM launched Palomar (palomar-registry.org), “the analogue of a preprint server for Lean proofs”.
Status
- Claim
Result confirmed
- Our reporting
- High confidence
- Verification
- Lean-verified
- Importance
- 3 of 5
- Last verified
- 29 October 2026
Your AI and this story
- GPT-6 Astra110 days after its cutoff
- Claude Opus 5.549 days after its cutoff
- Gemini 4 Hydrogen140 days after its cutoff
- Grok 4.779 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 49 days before it.
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
- 29 Oct 2026: Google DeepMind’s formal-conjectures repository made Palomar links mandatory: a new linter (linter.style.formal_proof_palomar, on by default) requires every formal proof of a ‘research solved’ problem, including conditional ones, to link to a Palomar entry; the 1,096 existing non-Palomar proof annotations on 1,070 declarations in 734 problem files got local opt-outs (commit d9f6ffa, PR #7631)
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.
Sources
6 sources from 3 sites. Numbers match the chips in the text.
6 sources: 6 primary
Primary
- Palomar registrypalomar-registry.org, official
- Terence Tao: Palomar, a registry of Lean-verified mathematicsterrytao.wordpress.com, official
- Palomar statementpalomar-registry.org, official
- GitHub: leanprover/comparatorgithub.com, code
- GitHub: mathlib-initiative/formalization.yamlgithub.com, code
- formal-conjectures commit d9f6ffa: add linter to enforce Palomar submissions (#7631)github.com, code
Changes
- Added formal-conjectures’ Palomar linter
- Filed