AI Now Writes Lean Proofs Faster Than Lean Can Check Them

<p>AI is getting better at writing mathematical proofs, which raises a question: can we keep up with checking what it writes? The usual answer is formal verification. The AI writes its proof as Lean code, Lean checks every step automatically, a proof that passes is correct, and machine checking is fast and cheap.</p> <p>We tested that answer on OpenAI's public library of AI-generated mathematics a

Read the source →