2020's Biggest Breakthroughs in Math and Computer Science

[Music] 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 touring 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 problems seem 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 [Music] this is henry yuen he's one of five co-authors of the proof 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 approver 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 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 uh spooky quantum mechanical fashion the policeman's job is to 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 touring's halting problem 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 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 picharillo was a graduate student when she first heard about the conway knot 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 like what's supposed to be so part about this problem and then the following week i had a meeting with cameron gordon a senior topologist in in my department um about something else and i mentioned it to him there he was like oh really you showed the conway nuts nut slice like show me um and then i started to put it up um and he started asking kind of detailed questions and then at some point he got he got very excited picturillo's proof was published in the annals of mathematics it was it was quite surprising to me i mean it's just one not in general when mathematicians prove things we 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 um so i do care about three and four dimensional spaces though um and it turns out that when you want to study three and four dimensional spaces you find yourself studying doubts 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 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 lead 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 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 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 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 and then we will be able to honestly say you know that it's as smart as an undergraduate in some sense you

Channel: Quanta Magazine

Views: 1,495,008

Rating: 4.9288116 out of 5

Keywords:

Id: HL7DEkXV_60

Length: 7min 46sec (466 seconds)

Published: Wed Dec 23 2020

Reddit Comments

[u/wintervenom123]

1. A landmark proof simply titled “MIP* = RE" establishes that quantum computers calculating with entangled qubits can theoretically verify the answers to an enormous set of problems. Along the way, the five computer scientists who authored the proof also answered two other major questions: Tsirelson’s problem in physics, about models of particle entanglement, and a problem in pure mathematics called the Connes embedding conjecture.

2. In February, graduate student Lisa Piccirillo dusted off some long-known but little-utilized mathematical tools to answer a decades-old question about knots. A particular knot named after the legendary mathematician John Conway had long evaded mathematical classification in terms of a higher-dimensional property known as “sliceness.” But by developing a version of the knot that yielded to traditional knot analysis, Piccirillo finally determined that the Conway knot is not “slice.”

3. For decades, mathematicians have used computer programs known as proof assistants to help them write proofs — but the humans have always guided the process, choosing the proof’s overall strategy and approach. That may soon change. Many mathematicians are excited about a proof assistant called Lean, an efficient and addictive proof assistant that could one day help tackle major problems. First, though, mathematicians must digitize thousands of years of mathematical knowledge, much of it unwritten, into a form Lean can process. Researchers have already encoded some of the most complicated mathematical ideas, proving in theory that the software can handle the hard stuff. Now it’s just a question of filling in the rest.

[u/DoktorLuciferWong]

The "I don't care about knots" remark lol

[u/MobiusLoops]

Not once did they mention the results of my thesis. Shameful :p

[u/Waldinian]

"imagine you have a police officer, and they're trying to interrogate two separate suspects, but the suspects are quantum entangled with each other."

Not sure where anyone was trying to go with that analogy. I guess your have try your best to explain your highly technical problem in the span of thirty seconds to a lay audience, but still.

[u/__ah]

Quanta magazine is great at scientific journalism, if you don't read their stuff consider checking it out

[u/cole-macgrath97]

Wow, Kevin Buzzard taught me M1F and algebraic geometry, I didn’t expect him to pop out in this video! Really enjoyed his lectures!! He started working on Lean and Xena 2 years ago though.

[u/[deleted]]

While Quanta is nice, I take them with a grain of salt. They mostly cover only what is simpler and sexier to explain, and take inspiration from a small number of blogs. They cover a small portion of mathematics, really.

Also, not so long ago they found a flaw in the first breakthrough, that is now claimed to be fixed. But it remains to be checked.

[u/junior_raman]

Thanks for sharing.