Palomar – a registry of Lean verified mathematics

• In recent months there has been a proliferation of AI-generated proofs of various old and new results, some of which have been formalized in the proof assistant language Lean.