Palomar: Registry of Lean Verified Mathematics

I'm Matt Wood, and this is For Your Information. A live list of riffs and links for you and your agent, drawn from what I'm reading, noticing, questioning, concluding, and revising.

Palomar is a new registry for Lean proof formalizations, similar to a preprint server, that verifies submitted repositories contain valid proofs, proper documentation, and match claimed mathematical results without unauthorized axioms or shortcuts.

terrytao.wordpress.com →

Connections

Supports

Introducing Dogwood: runtime verification for AI agents Dogwood provides runtime verification for AI agents; Palomar provides static verification of mathematical proofs — both represent a broader trend toward verified/trustworthy computational artifacts, with Palomar potentially serving as a ground-truth source for AI mathematical reasoning.
Leiden Declaration on Artificial Intelligence and Mathematics The Leiden Declaration on AI and Mathematics directly relates to Palomar's mission — Palomar provides concrete infrastructure for verified mathematical knowledge that the Declaration advocates for, offering a trustworthy registry where AI-assisted proofs can be validated and preserved.

Related to

Formal Methods at Jane Street: Agentic Coding Changes the Calculus Jane Street's formal methods work explicitly involves Lean and agentic coding; Palomar as a registry for Lean formalizations would be a natural publication venue for the kind of verified code/math artifacts Jane Street's formal methods teams produce.

Challenges

The Zero-Cost Fallacy: Open Source in the Agentic Era (Thoughtworks) Palomar's preprint-server model for verified mathematics challenges the 'zero-cost fallacy' argument by demonstrating open, community infrastructure that has genuine validation overhead and quality guarantees beyond typical open source repositories.

Type:	link
First published:	Wednesday, 19 August 2026 at 16:28 UTC
Location:	https://terrytao.wordpress.com/2026/08/18/palomar-a-registry-of-lean-verified-mathematics/
URL:	https://mattwood.fyi/i/eaa9aff9