## Link https://youtu.be/E9WIP5YqQt8 ## Clips ### Somehow set theory won, for some random reason. start = 3:20 end = 4:20 ### The software I just showed you is called Lean. Major mathematics funding agencies are now involved start = 13:40 end = 15:40 ### Everything is wrong! start = 17:06 end = 20:06 ### Turned my idea of what was easy and hard in mathematics upside down start = 25:00 end = 27:00 ### We think counting is easy but counting is EXTREMELY difficult! start = 26:22 end = 29:20 ### By the time we got to the stuff I thought was hard, it was REALLY REALLY easy to do in the theorem prover. Students formalized Atiyah-McDonald's Commutative Algebra. Then we did Schemes! start = 29:15 end = 31:20 ### So I proudly announced on the Lean chat that we had defined schemes and the computer scientists just looked at it like what? It was the definition of a thing. start = 31:20 end = 32:30 ### Then I went around telling Algebraic Geometers that I'd just taught a computer the meaning of "Let X be a Scheme" and they laughed and didn't care either. start = 32:20 end = 33:10 ### So I proved that affine schemes are schemes, which was trivial. And that made infinitely many schemes. Then the computer scientists said great it's ready for publication in a computer science journal, and I told them "But it's trivial!" start = 33:00 end = 34:30 ### So we started breaking new ground completely by accident start = 34:30 end = 34:40 ### By biggest regret is that I never got to talk to Voevodsky about this, two months after I started playing with Lean, Voevodsky died, so I never got to ask him why he never defined schemes. I think he'd lost interest in Algebraic Geometry, I think he'd become a constructivist, he got interested in Foundations of Mathematics start = 34:30 end = 35:20 ### I'd formalized 5 pages of Grothendieck's EGA, so there was quite a lot left start = 35:10 end = 36:10 ### Then a Fields medal was awarded for Perfectoid spaces, so I thought I'll define that and we'll crack the Algebraic Geometers and get them interested that way start = 36:00 end = 37:20 ### This software has existed for 50 years and mathematicians have been completely ignoring it start = 36:40 end = 39:00 ### Mathlib is a 21st century version of Bourbaki, and the way it's written is very similar to the Bourbaki style. We had to develop the theory of Topological Vector Spaces before the basic theorem of integration. (This backwardness is clearly a "small" issue in the same sense as Kelvin's "two clouds" that led to relativity and quantum mechanics. This seemingly small issue suggests a possible future involving localized formalization, many smaller distributed mathlibs rather than a large centralized one, and the need to support that sort of system is a strong argument for needing not just an intuitionistic logic (which these systems already have) but a paraconsistent one at the foundations, namely a logic that can handle small contradictions between (say) the definition of a ring in one place and another without having to call them by different names, the bits imported from different places must be allowed to evolve independently and even to contradict each other in their use of terminology and definitions without the whole system becoming trivial. This has always been how mathematics worked when it was running on paper and human minds, and it's one of the least recognized steps that will need to be formalized to understand precisely what mathematics is) start = 49:25 end = 51:00 ### Scholze realizing that most people who said they'd read his paper had not read the most technical lemma of the paper and he came to believe that no one had actually read it start = 59:12 end = 1:00:50