Palomar registry opens for Lean verified mathematics submissions

The Palomar registry of Lean verified mathematics has opened for submissions. Incubated by the Lean Foundation for Open Research (Lean FRO) and ICARM, the registry serves as a repository for external GitHub snapshots containing Lean code that adheres to formalization best practices.

To ensure clarity and prevent errors such as the addition of unauthorized axioms, Palomar requires specific components for submissions: a human-readable challenge file, a solution module containing the proof, and a metadata file describing the results in informal language. The initiative aims to act as a preprint server for verified mathematical proofs.