TED Talks Daily - The path to mathematical superintelligence | Tudor Achim

Episode Date: July 3, 2026

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. Hosted on Acast. See acast.com/privacy for more information.

You're listening to TED Talks Daily, where we bring you new ideas and conversations to spark your curiosity every day. I'm your host, Elise Hew. As AI becomes more intertwined in every aspect of our lives, humanity and science are facing a huge new truth problem. The tools we're increasingly relying on to accelerate discovery, such as generative AI and large language models. Well, they have a habit of completely making things up. We simply don't have the human bandwidth. to review all these proofs? Are we resigned to drown in a sea of unverified claims where we can't really tell truth from fiction? That was computer scientist Tudor Akeem, and yes, he's talking about AI hallucinations.

For most applications, these far-fetched inventions might be inconvenient or confusing, but for science, they could be catastrophic. In this talk, he shares why he thinks a 400-year-old idea holds the fix. The German mathematician Leibniz's dream of a logical framework where errors are simply impossible. He makes the case that grounding AI in this formal mathematical verification could transform it from unreliable chatbots into rigorous partners for scientific discovery. The talk is coming up right after a short break. And now our TED Talk of the Day. Let's take a look at this clay tablet. It might not look like much, but it's actually some of the old.

The oldest mathematics we have. It's a 4,000-year-old message in a bottle from ancient Babylon, a precursor to the quadratic equation. And for four millennia, people have been doing math basically the same way. Someone will have a brilliant idea, they'll write it down, and their peers will discuss and check it. It's a process built on creativity, communication, and most importantly, trust between people.

And what might seem like a humble or simple process is anything but. It's not just been successful. It's been, as the physicist Eugene Wigner famously put it, unreasonably effective. Wigner was pondering and trying to unravel a deep mystery. Why should the abstract, creative, and often bizarre ideas that spring from a mathematician's imagination so often be the perfect language with which we understand the universe?

why should the strange laws of non-Euclidean geometry, which were originally conceived of as a thought experiment in the 19th century, turn out to be the exact mathematics that Einstein needed for general relativity? Why should the esoteric math of group theory, which was originally designed to study the abstract nature of symmetry, be fundamental to understanding everything from particle physics to the patterns and crystals? Well, there's no logical reason it has to be this way.

This strange connection between pure mathematical thought and the real world has actually been the invisible engine driving human progress. Every piece of technology that defines our lives was ignited with a mathematical spark. If you take the device in your phone, its brain is based on the quantum mechanics of semiconductors, and that's a theory built on linear algebra and complex numbers. The wireless signals that get data. to it. They're just a concrete manifestation of Maxwell's equations. And finally, the security that protects your data online

is based on number theory, which for a long time was truly considered the most pure and least applicable possible branch of mathematics. And now it safeguards trillions of dollars in the global economy. And now we come to AI. Modern AI is not just built with math, it's forged from it. forged from it. A neural network is just a monumental structure of applied mathematics, and when AI's learn, they're using the tools of calculus to navigate vast landscapes of possibilities with billions of dimensions.

So AI is, in its soul, a mathematical idea that's given life through computation. So we agree that math is the foundation that modern civilization is based on. But that foundation is starting to show some signs of strain. strain. The very process of human-led discovery that's gotten us to this point is nearing a breaking point buckling under the weight of its own success. And now AI, which is one of mathematics's greatest creations, is accelerating us towards that breaking point faster than the world's ready for. So let's just look at some evidence. Consider the Poincerey conjecture. This is a legendary problem. It's a fundamental question about the nature of three-dimensional shapes, originally posed in

in 1904. And for nearly a century, it stood as an unconquered Everest of mathematics. Until in 2002, a Russian mathematician working in isolation named Gregori Perilman posted a series of three short cryptic papers online. He didn't bother submitting it to a journal. He just put them on the Internet and walked away. His fellow mathematicians had to stop what they were doing and try to decipher it. And several teams working independently of the best apologist in the world took the next four years to try to unpack the arguments, fill in the logical gaps, and eventually at the end, after they really reviewed it, declared that yes, he did it. He proved the Poincere conjecture. But that's interesting, because it took one person to write a

proof and a global, multi-year intellectual mobilization to check it. And that's in the best case, when the proof is correct. Consider Andrew Wiles as proof of for Ma's last theorem. With the electrifying announcement in 1993 in Cambridge, the world celebrated. But during the peer review process, deep in it, a single thread was found out of place in that magnificent tapestry of a proof,

and when we started to pull on it, the proof started to unravel, and this wasn't a small mistake. Andrew Wiles and his collaborator, Richard Taylor, took two years of heroic secret effort to try to fix it. And that effort included some insights, that Andrew Wiles said were among the most important in his life. And that's before we throw AI into the mix.

Two short years ago, AI could barely solve entry-level high school math contest problems. They were very clever, but brittle. Now, in 2025, they can compete with the best of us at the International Math Olympiad, which is the premier pre-college math competition. But the interesting bit is the following. The AI might work for four hours and produce a purported solution, which takes an expert human mathematician, maybe up to an hour to check. And we all know the exponential trend that AI is on.

So we can expect it's not going to be one proof in an afternoon. It's going to be 1,000 pretty soon. And they're not going to be attempts to solve math contest problems. They're going to be attacks on the most fundamental and important questions of the day. whether it's the Riemann hypothesis, Navier-Stokes, or P versus N.P. Just to pick a few. We simply don't have the human bandwidth to review all these proofs. There's only a couple thousand mathematicians that are qualified to do it,

and they already have day jobs. And it's not just a verification bottleneck. The very process by which we train these AIs is taking the data off the Internet, which is from humans, post-training them with human feedback, and so we're essentially baking in the cognitive biases and the flawed reasoning of humans into these future engines of discovery. So the conclusion is in some sense obvious.

Humans are becoming the bottleneck of verification for AI. Another question is, where does that leave us? Is this the end of the road for a reliable mathematical discovery? Are we resigned to drown in a sea of unverified claims where we can't really tell truth from fiction? And are we about to squander the opportunity for AI to revolutionize math? Well, the good news is no. but it does mean it's time to upgrade the 4,000-year-old operating system of math

and move away from the imprecise and ambiguous nature of human language and towards a language that computers can understand. The solution is formal mathematics. But before I tell you how this futuristic idea works, we should first recognize that it has a deep and fascinating history dating back to the 17th century where a mathematician actually laid out the roadmap with stunning foresight. 400 years ago, in a Europe, torn by religious and political conflict,

a polymath named Gottfried Wilhelm Leibniz, had a vision of breathtaking ambition. He was a contemporary of Newton and a co-creator of calculus, but his dreams went far beyond that. He dreamed of something called a universal characteristic, which was a system for perfectly encoding, all scientific and philosophical thought. And the system had three parts.

First, you need a perfect logical language. Second, you need a grand encyclopedia written that language that contains all verified human thought. And third, and this is the master stroke, you need a so-called engine of reason, a system of mechanical rules by which you can automatically derive new facts from that library as surely as a calculator performs arithmetic.

Now, Leibniz thought this would revolutionize humanity. With a system like this, if two people had an intellectual conflict, they would resort to logic and not rhetoric to resolve it. They would simply sit down, say, Calculemos, let us calculate, and get to the bottom of it. In some sense, it was meant to be a universal calculator for truth. Now, Leibniz was a bit of an optimist. He thought this would take a small group of people five years

to build, and he was off by several centuries. But what I think is really remarkable is that in 2025, truly for the first time in history, it's actually possible to realize this philosopher's dream. So what do we need? Well, we need a perfect logical language. Turns out we've got it. It's called Lean. Lean is a programming language, but it's also what's known as a proof assistant. You can think of it as a programming environment for mathematical proofs where it doesn't just give you feedback if you have a syntax error here or there, it's actually looking at the core of the mathematical argument and telling you if you have any problems anywhere in it. Great. What's the second thing we need? We need the grand encyclopedia. Well, the good news is we've got that too. It's called Mathlib. Mathlib is an

open source project. It's about two million lines of code in lean, and it covers a lot of the undergraduate and graduate math curriculum. You can think of it like a Wikipedia for proven truth where every edit is computationally certified for correctness. Okay. We've got the language, we've got the encyclopedia,

what about the engine of reason? Well, we could try to have humans to it, but you've got to write a lot of lean code, and the level of robotic precision you need to write a formal proof is not something that human creativity is so well suited for. And that's how we've come full circle. It turns out that AI is the key to making this whole thing work.

In the future, AI is not just going to be writing math papers in English for humans to read. They're going to be writing math proofs and lean for computers to check. And that is the fundamental key that makes it possible to use Leibniz's vision to unlock the full potential of AI in mathematics. Because when a math AI spits out a proof in lien of, let's say, the Riemann hypothesis, we're not going to need humans to go through every single line of the proof in painstaking detail, check every single case, and understand the possibly strange and alien logic of the proof just to see if it's correct.

Instead, all we're going to do is we're going to take those files, we're going to give them to a lien compiler, and if it builds, we can know with absolute certainty it's correct. And this is what fundamentally altered. our relationship with AI. AI can now become a true collaborator, one whose word we don't have to take on blind faith. We get to trade in the tedium of checking

for the creative joy of discovery. Humans get to use our intuition and judgment. We ask the questions, we chart the course, we propose the brilliant conjectures, and then we delegate to AI to explore the vast oceans of logic to find the correct answer, and then a computer confirms that we've gotten to the destination.

And the amazing thing is that this isn't just some far-off science fiction dream. It turns out that at this year's International Math Olympiad, automated systems were able to find solutions to five of the six problems in a way that computers could check and require no human review whatsoever. And that's enough to get a gold medal level performance. So the transition's already happening. So are humans going to be the bottleneck for math research? Well, the answer is yes, but only if we refuse to change, only if we insist on being the only

thinkers and the only checkers. But if we're able to realize this 400-year-old vision, we're not going to replace ourselves, we're going to elevate ourselves. We're going to put ourselves in the driver's seat as the explorers, the architects, and the question askers. And that means that formal mathematics is the key to this new era of discovery based on the powerful and essential partnership between human imagination and mathematical superintelligence.

Thank you. That was Tudor Akeem at TED AI in San Francisco, California in 2025. If you're curious about Ted's curation, visit TED.com slash curation guidelines. And that's it for today. Ted Talks Daily is a podcast from TED. This episode was produced and edited by our team, Martha Estefanos, Oliver Friedman, Lucy Little, Emma Tobner, and Tonzika Sungmar Nivon. Additional support from Daniela Ballereseo, Christopher Faisi Bogan, Valentina Bohanini, Ban Ban Chang, Brian Green, and Laney Lott.

Learn more at podcasts.com. I am Elise Hupe. I'll be back tomorrow with a fresh idea for your feet. Thanks for listening.