Home
Login
Register
The Path to Mathematical Superintelligence | Tudor Achim | TED - Video học tiếng Anh
Practice Listening
Practice Listening
/
Video
/
TED Talk
/
The Path to Mathematical Superintelligence | Tudor Achim | TED
The Path to Mathematical Superintelligence | Tudor Achim | TED
Select learning mode:
View subtitles
Pick word
Rewrite word
Highlight:
3000 Oxford Words
4000 IELTS Words
5000 Oxford Words
3000 Common Words
1000 TOEIC Words
5000 TOEFL Words
Subtitles (262)
0:04
Let's take a look at this clay tablet.
0:06
It might not look like much,
0:08
but it's actually some of the oldest mathematics we have.
0:11
It’s a 4,000-year-old message in a bottle from ancient Babylon --
0:15
a precursor to the quadratic equation.
0:18
And for four millennia,
0:20
people have been doing math basically the same way.
0:23
Someone will have a brilliant idea,
0:25
they’ll write it down, and their peers will discuss and check it.
0:30
It’s a process built on creativity, communication and, most importantly,
0:35
trust between people.
0:37
And what might seem like a humble or simple process is anything but.
0:42
It's not just been successful.
0:44
It's been, as the physicist Eugene Wigner famously put it,
0:48
unreasonably effective.
0:50
Wigner was pondering and trying to unravel a deep mystery.
0:54
Why should the abstract, creative,
0:57
and often bizarre ideas that spring from a mathematician's imagination
1:01
so often be the perfect language with which we understand the universe?
1:06
Why should the strange laws of non-Euclidean geometry,
1:09
which were originally conceived of as a thought experiment
1:12
in the 19th century,
1:13
turn out to be the exact mathematics
1:15
that Einstein needed for general relativity?
1:17
Why should the esoteric math of group theory,
1:20
which was originally designed to study the abstract nature of symmetry,
1:24
be fundamental to understanding everything from particle physics
1:28
to the patterns in crystals?
1:30
Well, there's no logical reason it has to be this way.
1:34
This strange connection
1:37
between pure mathematical thought and the real world
1:41
has actually been the invisible engine driving human progress.
1:45
Every piece of technology that defines our lives
1:49
was ignited with a mathematical spark.
1:52
If you take the device in your phone,
1:54
its brain is based on the quantum mechanics of semiconductors.
1:57
And that's a theory built on linear algebra
2:00
and complex numbers.
2:02
The wireless signals that get data to it,
2:04
they're just a concrete manifestation of Maxwell's equations.
2:08
And finally, the security that protects your data online
2:13
is based on number theory,
2:15
which for a long time was truly considered the most pure
2:18
and least applicable possible branch of mathematics.
2:22
And now it safeguards trillions of dollars in the global economy.
2:27
And now we come to AI.
2:29
Modern AI is not just built with math, it's forged from it.
2:34
A neural network is just a monumental structure of applied mathematics.
2:38
And when AIs learn,
2:40
they're using the tools of calculus
2:42
to navigate vast landscapes of possibilities
2:44
with billions of dimensions.
2:46
So AI is, in its soul,
2:49
a mathematical idea that's given life through computation.
2:53
So we agree that math is the foundation that modern civilization is based on.
2:59
But that foundation is starting to show some signs of strain.
3:03
The very process of human-led discovery
3:06
that's gotten us to this point is nearing a breaking point,
3:09
buckling under the weight of its own success.
3:11
And now AI, which is one of mathematics’ greatest creations,
3:15
is accelerating us towards that breaking point
3:17
faster than the world's ready for.
3:19
So let's just look at some evidence.
3:21
Consider the Poincaré conjecture.
3:24
This is a legendary problem.
3:26
It's a fundamental question
3:27
about the nature of three-dimensional shapes
3:30
originally posed in 1904.
3:32
And for nearly a century,
3:34
it stood as an unconquered Everest of mathematics.
3:38
Until in 2002,
3:40
a Russian mathematician working in isolation
3:42
named Grigori Perelman
3:44
posted a series of three short, cryptic papers online.
3:48
He didn’t bother submitting them to a journal --
3:50
he just put them on the internet and walked away.
3:52
His fellow mathematicians had to stop what they were doing
3:55
and try to decipher it.
3:57
And several teams working independently of the best of colleges in the world,
4:02
took the next four years to try to unpack the arguments,
4:05
fill in the logical gaps
4:07
and eventually, at the end, after they really reviewed it,
4:10
declare that yes, he did it.
4:11
He proved the Poincaré conjecture.
4:14
But that's interesting
4:15
because it took one person to write a proof
4:20
and a global, multi-year intellectual mobilization to check it.
4:25
And that's in the best case, when the proof is correct.
4:29
Consider Andrew Wiles's proof of Fermat's Last Theorem.
4:32
With the electrifying announcement in 1993 in Cambridge, the world celebrated.
4:36
But during the peer-review process, deep in it,
4:40
a single thread was found out of place
4:42
in that magnificent tapestry of a proof,
4:45
and when we started to pull on it,
4:46
the proof started to unravel.
4:48
And this wasn't a small mistake.
4:50
Andrew Wiles and his collaborator Richard Taylor took two years of heroic,
4:56
secret effort to try to fix it.
4:58
And that effort included some insights that Andrew Wiles said
5:02
were among the most important in his life.
5:05
And that's before we throw AI into the mix.
5:08
Two short years ago,
5:10
AI could barely solve entry-level high school math-contest problems.
5:15
They were very clever, but brittle.
5:18
Now, in 2025,
5:20
they can compete with the best of us
5:22
at the International Math Olympiad,
5:24
which is the premier precollege math competition.
5:28
But the interesting bit is the following.
5:30
The AI might work for four hours and produce a purported solution,
5:36
which takes an expert human mathematician maybe up to an hour to check.
5:41
And we all know the exponential trend that AI is on.
5:44
So we can expect it’s not going to be one proof in an afternoon --
5:49
it’s going to be a thousand pretty soon.
5:51
And they're not going to be attempts to solve math-contest problems.
5:55
They're going to be attacks on the most fundamental
5:57
and important questions of the day,
5:59
whether it's the Riemann hypothesis,
6:01
Navier-Stokes or P versus NP,
6:04
just to pick a few.
6:05
We simply don't have the human bandwidth
6:08
to review all these proofs.
6:10
There's only a couple thousand mathematicians
6:12
that are qualified to do it, and they already have day jobs.
6:15
And it's not just a verification bottleneck.
6:17
The very process by which we train these AIs
6:20
is taking the data off the internet,
6:22
which is from humans,
6:23
post-training them with human feedback,
6:25
and so we're essentially baking in the cognitive biases
6:28
and the flawed reasoning of humans into these future engines of discovery.
6:32
So the conclusion is in some sense obvious.
6:36
Humans are becoming the bottleneck of verification for AI.
6:40
And now the question is, where does that leave us?
6:42
Is this the end of the road for reliable mathematical discovery?
6:46
Are we resigned to drowning in a sea of unverified claims
6:49
where we can't really tell truth from fiction?
6:51
And are we about to squander the opportunity
6:53
for AI to revolutionize math?
6:55
Well, the good news is no.
6:58
But it does mean it's time
6:59
to upgrade the 4,000-year-old operating system of math,
7:02
and move away from the imprecise and ambiguous nature of human language,
7:08
and towards a language that computers can understand.
7:12
The solution is formal mathematics.
7:16
But before I tell you how this futuristic idea works,
7:19
we should first recognize that it has a deep and fascinating history
7:23
dating back to the 17th century,
7:26
where a mathematician actually laid out the road map with stunning foresight.
7:30
Four hundred years ago,
7:32
in a Europe torn by religious and political conflict,
7:35
a polymath named Gottfried Wilhelm Leibniz
7:39
had a vision of breathtaking ambition.
7:42
He was a contemporary of Newton and a cocreator of calculus,
7:46
but his dreams went far beyond that.
7:49
He dreamed of something called a universal characteristic,
7:52
which was a system for perfectly encoding all scientific
7:56
and philosophical thought.
7:58
And the system had three parts.
8:01
First, you need a perfect logical language.
8:05
Second, you need a grand encyclopedia written in language
8:09
that contains all verified human thought.
8:13
And third,
8:14
and this is the masterstroke,
8:16
you need a so-called engine of reason,
8:18
a system of mechanical rules
8:20
by which you can automatically derive new facts from that library
8:24
as surely as a calculator performs arithmetic.
8:27
Now, Leibniz thought this would revolutionize humanity.
8:31
With a system like this,
8:33
if two people had an intellectual conflict,
8:35
they would resort to logic and not rhetoric to resolve it.
8:38
They would simply sit down,
8:39
say “calculemus” -- “let us calculate,”
8:42
and get to the bottom of it.
8:44
In some sense, it was meant to be a universal calculator for truth.
8:48
Now, Leibniz was a bit of an optimist.
8:51
He thought this would take a small group of people five years to build,
8:55
and he was off by several centuries.
8:58
But what I think is really remarkable
9:00
is that in 2025,
9:02
truly for the first time in history,
9:04
it's actually possible to realize this philosopher's dream.
9:08
So what do we need?
9:09
Well, we need a perfect, logical language.
9:12
Turns out we've got it.
9:14
It's called Lean.
9:15
Lean is a programming language,
9:17
but it's also what's known as a proof assistant.
9:20
You can think of it as a programming environment
9:23
for mathematical proofs,
9:25
where it doesn't just give you feedback
9:26
if you have a syntax error here or there --
9:28
it's actually looking at the core of the mathematical argument
9:31
and telling you if you have any problems anywhere in it.
9:34
Great.
9:35
What's the second thing we need?
9:37
We need the grand encyclopedia.
9:39
Well, the good news is we've got that too.
9:41
It's called Mathlib.
9:43
Mathlib is an open-source project.
9:45
It's about two million lines of code in Lean,
9:48
and it covers a lot of the undergraduate and graduate math curriculum.
9:53
You can think of it like a Wikipedia for proven truth,
9:57
where every edit is computationally certified for correctness.
10:02
OK, we've got the language,
10:04
we've got the encyclopedia,
10:05
what about the engine of reason?
10:08
Well, we could try to have humans do it,
10:10
but you've got to write a lot of Lean code
10:12
and the level of robotic precision you need to write a formal proof
10:16
is not something that human creativity is so well suited for.
10:19
And that's how we've come full-circle.
10:22
It turns out that AI is the key to making this whole thing work.
10:26
In the future, AI is not just going to be writing math papers in English
10:30
for humans to read.
10:31
They're going to be writing math proofs in Lean
10:34
for computers to check.
10:37
And that is the fundamental key
10:39
that makes it possible to use Leibniz's vision
10:42
to unlock the full potential of AI in mathematics.
10:46
Because when a math AI spits out a proof in Lean of, let's say,
10:50
the Riemann hypothesis,
10:52
we're not going to need humans to go through every single line of the proof
10:56
in painstaking detail,
10:57
check every single case,
10:58
and understand the possibly strange and alien logic of the proof
11:03
just to see if it's correct.
11:04
Instead, all we're going to do is we're going to take those files,
11:07
we're going to give them to a Lean compiler, and if it builds,
11:10
we can know with absolute certainty it's correct.
11:13
And this is what fundamentally alters our relationship with AI.
11:18
AI can now become a true collaborator,
11:20
one whose word we don't have to take on blind faith.
11:24
We get to trade in the tedium of checking for the creative joy of discovery.
11:30
Humans get to use our intuition and judgment,
11:33
we ask the questions,
11:35
we chart the course, we propose the brilliant conjectures
11:38
and then we delegate to AI to explore the vast oceans of logic,
11:43
to find the correct answer,
11:44
and then a computer confirms that we've gotten to the destination.
11:48
And the amazing thing
11:49
is that this isn't just some far-off science-fiction dream.
11:52
It turns out that at this year’s International Math Olympiad,
11:55
automated systems were able to find solutions to five of the six problems
11:59
in a way that computers could check and require no human review whatsoever.
12:03
And that’s enough to get a gold-medal-level performance.
12:06
So the transition is already happening.
12:09
So are humans going to be the bottleneck for math research?
12:15
Well, the answer is yes, but only if we refuse to change.
12:18
Only if we insist on being the only thinkers
12:21
and the only checkers.
12:23
But if we're able to realize this 400-year-old vision,
12:26
we're not going to replace ourselves,
12:28
we're going to elevate ourselves.
12:30
We're going to put ourselves in the driver's seat
12:32
as the explorers, the architects and the question askers.
12:35
And that means that formal mathematics is the key to this new era of discovery,
12:39
based on the powerful and essential partnership between human imagination
12:43
and mathematical superintelligence.
12:47
Thank you.
12:48
(Applause)
