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

_Tuesday, August 18, 2026 at 10:40 PM 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
Retrieved: 2026-08-19T10:09:01.492Z
Publisher: Tech & Business (techandbusiness.org)