Palomar, a registry for Lean-verified mathematics incubated by the Lean FRO and ICARM, has opened for submissions. It records fixed GitHub repository snapshots containing formal Lean proofs of old or new mathematical results, including work produced by humans, AI systems, or both. Terence Tao serves on its scientific advisory board alongside Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Ravi Vakil, and Akshay Venkatesh. Each submission must include a challenge file that states the claimed results in human-readable Lean, a solution module containing proofs, and a formalization.yaml metadata file with an informal description and disclosures. Palomar mechanically uses Lean Comparator to verify that the solution typechecks and proves the challenge file’s statements. A large language model separately assesses whether the informal description appears to match those formal statements, while the registry also checks minimal repository standards. Registration does not constitute peer review for novelty, interest, or mathematical accuracy. Tao reported successfully submitting his recent Lean formalization of the proof of Sendov’s conjecture as a test and plans to submit older formalizations. AI agents can assist with submission mechanics, though Palomar recommends human review.