Registry of Lean-verified mathematics

Palomar records mathematical claims from fixed versions of their source files, checks their proofs with Lean, and publishes the exact statement, the libraries it uses, and the review's comments.