Palomar – a registry of Lean verified mathematics
Summary
Terence Tao announces Palomar, a registry for Lean-verified mathematics. The post describes how Palomar will verify Lean proofs (typechecking and alignment with informal descriptions) using mechanical checks and an LLM for non-deterministic matching, and invites submissions while noting it is not a peer-reviewed journal.