Who Verifies the Verifier [Korbonits]

[mklabgr]

Summary

• [b]The Progress: Google DeepMind successfully used an AI agent to solve several open mathematics problems by writing proofs directly in Lean (a formal proof language).[/b]
  
• [b]The Benefit: Because the AI operates in a loop with a compiler, it can't "cheat" or hallucinate. The compiler provides absolute mathematical verification for pennies, removing the need for scarce human expert reviewers.[/b]
  
• [b]The Limit: The AI can only solve problems that are already translated into Lean.[/b]
  
• [b]The New Bottleneck: The bottleneck has shifted from verifying proofs to translating complex human mathematics into formal code so the compiler can read them.[/b]
  

ARTICLE