---
id: "2026-08-18-palomar-lean-registry"
url: "https://postcutoff.com/e/2026-08-18-palomar-lean-registry/"
as_of: "2026-11-13T13:49:00+01:00"
date: "2026-08-18"
date_precision: day
category: science
importance: 3
confidence: high
status: [Result confirmed]
verification: Lean-verified
sources: 6
editor: human editor
human_review: null
version: "2026-10-29"
---

As of: 2026-11-13 13:49 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-08-18-palomar-lean-registry/

# 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
- 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.

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 110 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 49 days after its cutoff
- Gemini 4 Hydrogen (training cutoff March 2026): 140 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 79 days after its cutoff

## Sources

1. [Palomar registry](https://palomar-registry.org/) (palomar-registry.org, official)
2. [Terence Tao: Palomar, a registry of Lean-verified mathematics](https://terrytao.wordpress.com/2026/08/18/palomar-a-registry-of-lean-verified-mathematics/) (terrytao.wordpress.com, official)
3. [Palomar statement](https://palomar-registry.org/statement) (palomar-registry.org, official)
4. [GitHub: leanprover/comparator](https://github.com/leanprover/comparator) (github.com, code)
5. [GitHub: mathlib-initiative/formalization.yaml](https://github.com/mathlib-initiative/formalization.yaml) (github.com, code)
6. [formal-conjectures commit d9f6ffa: add linter to enforce Palomar submissions (#7631)](https://github.com/google-deepmind/formal-conjectures/commit/d9f6ffa8dd7fc2b8b597dd1f7a824d27b12b88af) (github.com, code)

## Changes

- 2026-10-29: Added formal-conjectures' Palomar linter
- 2026-09-29 (filed): Created

## Related

- 2026-09-18: [SAIR launches the Open Math Model initiative for community-governed open-weight math AI, plus Lean Kernel and Andrews–Curtis challenges](https://postcutoff.com/e/2026-09-18-sair-open-math-model-initiative/index.md)
- 2026-08-05: [Sendov's 1958 conjecture on polynomial roots proved with GPT-5.6 Pro](https://postcutoff.com/e/2026-08-05-sendov-conjecture-proved/index.md)
- People: [Terence Tao](https://postcutoff.com/person/terence-tao/)