Palomar: A registry of Lean verified mathematics

Terence Tao announces the opening of Palomar, a registry for Lean-verified mathematics designed to address the proliferation of AI-generated proofs by providing a standardized way to verify that Lean code actually proves claimed mathematical results. Palomar requires submissions to include a challenge file with human-readable result descriptions, a solution module with the formal proof, and a metadata file with informal descriptions, with automated mechanical checks and AI-assisted review to ensure validity and that formal statements match their informal descriptions.