+- MKLab (https://mklab.gr)
+-- Forum: ΚΑΤΑΛΟΓΟΣ (INDEX) (https://mklab.gr/forumdisplay.php?fid=1)
+--- Forum: TEXNHTH NOHMOΣΥΝΗ (AI) (https://mklab.gr/forumdisplay.php?fid=5)
+---- Forum: ΑΡΘΡΑ (ARTICLES) (https://mklab.gr/forumdisplay.php?fid=33)
+---- Thread: Who Verifies the Verifier [Korbonits] (/showthread.php?tid=185)
Who Verifies the Verifier [Korbonits] - mklabgr - 06-09-2026
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