Palomar opens Lean-proof registry with mechanical and AI checks

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.