Palomar – a registry of Lean verified mathematics
terrytao.wordpress.com
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. However, checking tha…