Palomar: A Notary for AI-Generated Proofs
Terry Tao and the Lean FRO launched Palomar on August 18 — a registry that runs submitted Lean proof repositories through a verification pipeline and publishes the exact formal statement, library dependencies, and reviewer comments. The project is a direct response to the surge in AI-generated Lean proofs, where the bottleneck has shifted from producing proofs to trusting them.
Read more →