Palomar launches a registry to validate AI-generated Lean math proofs
Palomar, a registry of Lean-verified mathematics incubated by Lean FRO and ICARM with Terry Tao on its board, is open for submissions. It snapshots GitHub repos, mechanically typechecks proofs against a challenge file, and run an LLM check that informal claims match. Think preprint server for machine-checked proofs, built for the surge of AI-generated ones.