In 1935, Albert Einstein was famously disturbed by an idea in quantum physics.
When two particles are quantum entangled,
they can instantaneously interact across vast distances.
Einstein found this phenomenon "spooky."
Just the next year,
Alan Turing identified a problem computers would never be able to solve.
Computers usually operate based on inputs and outputs,
but sometimes they can get stuck in infinite loops.
Turing proved there's no way to tell when this will happen,
and he called it the halting problem.
Today we recognize it in the Spinning Wheel of Death.
In the 1930s, quantum entanglement and the halting problem seemed to have nothing to do with each other.
But this year, they combined in a landmark proof
that set off a cascade of solutions to open problems in computer science, physics and mathematics.
This is Henry Yuen.
He's one of five co-authors of the proof.
Yuen: You know, what this paper is about, it's in computational complexity theory,
which is like a branch of theoretical computer science.
And it talks about the computational
power of a model of what's called interactive proofs.
An interactive proof is a kind of logical interrogation method that models computation as the exchange of messages between two parties
-- a prover, and a verifier.
To understand how this works,
imagine the verifier is a police officer interrogating two subjects: The provers.
You can't go out and confirm every single detail of the suspect's stories,
but by asking the right questions and pitting your subjects against each other,
you can catch them in a lie
or develop confidence that the facts check out.
Yuen: The policemen will place these two suspects in different rooms,
but it just so happens that these suspects also can share quantum entanglement to coordinate their responses in some spooky quantum mechanical fashion.
Yuen: The policeman's job is to try to figure out what the truth really is.
The main result of this paper is that even though the these suspects
might share quantum entanglement, the policemen can actually
interrogate them in such a way that the policemen can figure out the truth of
any mathematical statement corresponding to
an enormously complicated range of questions.
This means that, in theory, a super powerful quantum computer could verify answers to even unsolvable problems like Turing's halting problem.
Yuen: It involves all these really beautiful pieces from different areas.
Things from computer science, things from mathematics and physics,
that you know before we didn't think were that related to each other, and yet they are.
I think it points to something much more interesting. I don't know what,
but you know there's a feeling that there's something more to,
you know, there's like a whole new world to discover.
This is John Horton Conway.
His infamous knot problem eluded mathematicians for half a century.
The question asked whether the Conway knot was actually a slice of a higher dimensional knot,
a property called sliceness.
This question proved answerable for thousands of similar knots, but Conway's resisted every attempt to untangle it.
Lisa Piccirillo was a graduate student when she first heard about the Conway knot.
Piccirillo: Well I just thought it was completely ridiculous
that we didn't know whether this knot was slice or not.
We have a lot of tools for doing this sort of thing, so i didn't understand like, why
for some 11-crossing-knot this should be so difficult.
I think the next day, which was a Sunday, I just started trying to run the approach
for fun and I worked on it a bit in the evenings just to try to see
what's supposed to be so hard about this problem.
And then the following week, I had a meeting with Cameron Gordon,
a senior topologist, in my department
about something else, and I mentioned it to him there.
He was like, "Oh really? You showed the Conway knot's not slice?" Like, show me.
And then I started to put it up and he started asking kind of detailed questions, and then
at some point he got, he got very excited.
Piccirillo's proof was published in the Annals of Mathematics.
Piccirillo: It was it was quite surprising to me.
I mean, it's just one knot.
In general,
when mathematicians prove things, we like to prove really broad, general statements:
All objects like this have some property. And I proved like, one knot has a thing.
I don't care about knots.
So, I do care about three and four dimensional spaces, though.
And it turns out that,
when you want to study three and four dimensional spaces, you find yourself studying knots anyway.
Mathematics can sometimes seem like a jumbled mosaic.
Major areas of study have never been fully written down,
and doing so would have required using thousands of other definitions that don't yet exist.
Now, imagine you had a Library of Alexandria that contained the entire history and the sum total of mathematical knowledge.
With everything catalogued, you could program an AI to verify increasingly complex proofs,
and one day, hopefully, come up with new ones on its own.
At Imperial College London, Kevin Buzzard is in the process of digitizing math.
He's teaching it to a software called Lean, which draws upon an ever-growing library of proofs and theorems.
Buzzard: I decided that this software was very interesting about three years ago,
and have since made a huge amount of noise about it.
We took some very, very modern mathematics and just
show, you know, we taught it to Lean and Lean could handle it.
And basically, it was at that point that I realized it should be able to do anything, really.
Lean has a big maths library, 450,000
lines of code long.
The library just grows all the time every day, you know,
10 more, 10 more pull requests get added to this library.
The growth is immense.
It's just slowly eating mathematics.
Buzzard: Computers speak a certain language,
so there's a fast-moving language which you have to learn.
And then once you've done that, you just explain the mathematics but in that language.
And the big problem is that in maths departments across the world,
we're teaching people the mathematical ideas,
but nobody's teaching them the language that these computers speak.
Buzzard: Mathematics is not quite what it's sold.
I mean, we tell the undergraduates that mathematics is this completely rigorous,
you know, theory built from the axioms.
And in practice, that's not how mathematics is done.
Computers are quite picky,
because they do want to know what's going on.
So one challenge we have faced, is that people are slightly imprecise,
and computers don't buy it.
Before you can teach something to the computer, you do need to understand it perfectly.
The act of engaging with the details can sometimes clarify the situation.
You end up with a proof which is slightly messy, and then you try and
type it into a computer and at the end of it, you end up with a with a slicker argument.
One of the goals is that we want to see an entire undergraduate curriculum in it.
And you know, give us another couple of years, and then we will be able to honestly say,
you know, that it's as smart as an undergraduate in some sense.