# Palomar opens Lean-proof registry with mechanical and AI checks

_Published Wednesday, August 19, 2026 at 4:17 AM EDT · Products, AI · Latest · Tier 2 — Notable_

Palomar, a registry for Lean-verified mathematics incubated by Lean FRO and ICARM, has opened for submissions. Entries are snapshots of GitHub repositories that include a challenge file, proof module and metadata. The registry uses Lean Comparator to check that a solution typechecks and proves the stated challenge; an LLM assesses whether the informal description appears to match it. Palomar says accepted entries are not peer reviewed for novelty, interest or accuracy.

## Sources

- [terrytao.wordpress.com](https://terrytao.wordpress.com/2026/08/18/palomar-a-registry-of-lean-verified-mathematics/)

---
Canonical: https://techandbusiness.org/newswire/E46doJ2Z_Loi38OGpAuuP8
Published: 2026-08-19T08:17:35.773Z
Story chronology: 2026-08-19T02:40:46.000Z
Retrieved: 2026-10-03T12:41:34.060Z
Publisher: Tech & Business (techandbusiness.org)