2020's Biggest Breakthroughs in Math and Computer Science - YouTube

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.