Generative AI hallucinates, creating a truth problem that science can't afford. Computer scientist Tudor Achim thinks a 400-year-old idea holds the fix: Leibniz's dream of a logical framework where errors are simply impossible. Learn about his idea for mathematical superintelligence that would ground AI in formal verification, turning unreliable chatbots into rigorous partners for scientific discovery.

The path to mathematical superintelligence

Mathematics has driven progress for thousands of years, but today, human verification can't keep up with the accelerating pace of AI-generated proofs. Legendary problems like the Poincaré conjecture took years for global teams to validate, while modern AI can now solve Olympiad-level challenges in hours. A 400-year-old vision of formalized logic, now realized through tools like Lean and Mathlib, promises certainty and trust in mathematical results. This shift lets humanity focus on creativity and exploration, while AI handles precision and proof verification.

AI And Formal Math Will End The Human Bottleneck In Discovery

For 4,000 years, math has relied on human trust and peer review, but the explosion of AI-generated proofs now overwhelms expert capacity to verify them. Legendary problems like the Poincaré conjecture already required years of collective scrutiny. A new era is emerging, where computers use formal languages like Lean to check proofs with absolute certainty. This shift could enable AI to collaborate reliably with humans, replacing tedious checking with creative exploration.