Latest / Strachey Lectures / Formalizing the Future: Lean’s Impact on Mathematics, Programming, and AI

Transcript

Formalizing the Future: Lean’s Impact on Mathematics, Programming, and AI · Strachey Lectures

• 0:01
  [Auto-generated transcript. Edits may have been applied for clarity.] So if you haven't.
• 0:15
  Okay. So welcome everybody to the day. So straight to lecture.
• 0:19
  So this is uh two distinguished lectures which are named after Christopher Straight genius who founded the programming research group here.
• 0:26
  And this is a particularly exciting lecture, uh, because we've got two lectures,
• 0:32
  both we had tomorrow and Kevin Bussard and, in my opinion, talking about it.
• 0:37
  In my opinion, the most interesting thing that's been happening in computer science, and that's the intersection, maybe even union in the last year.
• 0:45
  So we're really, um, very, very happy to have them here.
• 0:49
  Um, so before I introduce the speakers, I want to thank, um, Oxford Asset Management, who's been funding the series since 2015.
• 0:57
  And we're really grateful for their support because, um, we get such amazing speakers, uh, thanks to them.
• 1:05
  And for any students and researchers that want to find out more about their company, you can do that after the second talk.
• 1:11
  Oh, it's a coffee. So the way we're going to do it is we are going to have Leo's talk first for about 45 minutes.
• 1:20
  Then we're going to have questions and answers, and there will be a microphone going around.
• 1:24
  And then we'll have the same thing. Um, for Kevin.
• 1:28
  Okay.
• 1:29
  So um, so I'm really, really happy to introduce Leo Dimora, who is the chief architect of the lean theorem prover, which we're going to hear about.
• 1:39
  Um, he's currently, uh, I can read it off, a senior principal applied scientist at MIT.
• 1:46
  And before that, he had a, um, a similar role at Microsoft.
• 1:50
  Now, actually, he's not only the person who, um, built the limit theorem prover, but actually lots of other theorem provers, too.
• 1:58
  And I was not here a list of, um, prizes for such work.
• 2:03
  Um, so he received the award in 2021 for pioneering contributions to the foundations of the theory and practice of satisfiability modulo theory.
• 2:16
  The high for Verification Conference award in 2010 for the most influential work in the last five years in verification,
• 2:24
  the Herb Brent Award for Distinguished Contributions to Automated Reasoning.
• 2:28
  That was in 2019, the Programming Language of Software Award of the ACM in 2015 for the Z3 theorem prover.
• 2:35
  So that's another theorem prover.
• 2:37
  And uh, we're really happy today to have him speaking to us about, uh, formalising the future and Lincoln's impact on mathematics programming.
• 2:45
  And I said, thank you, thank you, thank you for such a kind introduction.
• 2:57
  Thank you very much. Uh, very happy to be here. And it's a pleasure to be here giving a talk with Kevin today.
• 3:05
  I want to tell you about Linc. Uh, that means whatever the reason, motivation for Linc was, uh, software verification, right?
• 3:15
  I mean, Z3 was very popular. It's bug finding bug finance.
• 3:20
  Microsoft was very influential there, but the goal was, can we make the same having the same success of such verification?
• 3:28
  We went through a very strange path from the heavy impacting mathematics that we never had dream of.
• 3:35
  Uh, but the goal. In both cases, it's like we both software.
• 3:44
  Mathematics in AI. Should they rely on manual review?
• 3:48
  Partial testing. I'm stating the theorem can be catastrophic or invalidates the whole results.
• 3:56
  Same thing for critical piece of software. Right.
• 3:59
  And one thing I see all the time, people fearing to make a change,
• 4:04
  a piece of software because they fear by making the change they may be introducing a bug.
• 4:10
  Especially if it's a critical piece of software. Uh, until you have machine checkable proofs.
• 4:17
  Right? You cannot. You don't need to check them only offline, but with also external checkers.
• 4:23
  And this of completely avoids the guesswork, right?
• 4:27
  You you create trusts. You have absolute trust now that your result is correct.
• 4:32
  And there are many consequences that we didn't expect.
• 4:36
  Like, it's not just about proving but about collaboration.
• 4:41
  And that's one of the messages we want to communicate today. These are open source programming language improv assistance.
• 4:50
  Right? Uh, and, I mean, we couldn't bring the impact he's having in mathematics software verification.
• 4:58
  I the project starting 2014, right.
• 5:02
  The goal at the time was to combine the automated interactive worlds.
• 5:06
  Uh, they're both called that three and linear are both called two improvers, but they are completely different beasts.
• 5:13
  Right. And the main thing is, are the machine checkable proofs.
• 5:18
  We say this eliminates the trust bottleneck, not a trust between humans.
• 5:23
  But now the trust between humans and machines AIS right in it opens up new possibilities for collaboration.
• 5:32
  Let's see an example here how link looks like this.
• 5:35
  If you substitute your codes, I think the community. This is the favourite edge story.
• 5:40
  This is by the community. You can use vim, you can use Emacs, but guess codes is the most usage one if you have an example.
• 5:49
  Very simple one. In lean you have libraries. Here we are importing math lib, the lean mathematical library.
• 5:57
  We have definitions. Definitions have names. It's called ODS.
• 6:00
  Here it states in this in a natural number these odds number.
• 6:05
  If there is a k such that's n equals two times k plus one writes the usual definition.
• 6:12
  Now that you have a definition, you can write theorems about this definition.
• 6:17
  Uh, you can give names to this to theorems like the name here is five is ODS and the claims that's five is ODS number.
• 6:25
  After you made a claim you can start trying to prove this is a proof.
• 6:29
  You're saying that's key is true. And link accepts it as a valid proof because five is two times two plus one.
• 6:37
  This is a proof that that's five sides a number. If you give an invalid proof link will complain.
• 6:42
  We are going to get a squiggly line. Now let's try to prove something more complicated is to make a point.
• 6:51
  That's leaves interactive again. I was very happy.
• 6:54
  It's funny when Kevin told me this. Told me that he started saying, I don't want to offend you, but these are my favourites.
• 7:03
  Computer game. And I was actually super happy when as a teenager, I loved to implement computer games.
• 7:11
  I never meant for my games when I was a teenager who were played by anybody but by myself.
• 7:17
  And now I found I finally built a game that had real users rights.
• 7:23
  And here on the right hand side, this is the board of the game.
• 7:28
  This is this. Like when you are playing chess, you have this state of the chess boards here.
• 7:34
  The right hand side is the board game. Let's see.
• 7:39
  We are going to start. The first move of this game is intro.
• 7:43
  We are trying to prove that if a number and odds this square is odds two, you're going to do introduction.
• 7:50
  We are giving name if n is item number these are k. We're giving a name k1.
• 7:56
  And we also give name to hypothesis. You're saying the hypothesis because we know for this k1 we know that m should be equal to two times k1 plus one.
• 8:09
  And we give a name here in one we can give names to hypothesis.
• 8:15
  Then we use the most popular move in the game.
• 8:18
  If you go to math lib you're going to find thousands and thousands applications of this move is the simplifier you are telling here.
• 8:29
  Need to apply simplification rules.
• 8:32
  Stirling. Also in the square brackets use E1B square telling you replace m by two times k1 plus one.
• 8:41
  You're also telling me intro expansion the definition of odds and number in ling.
• 8:47
  Maxine Greene. The part of the game board that has been modified in this game boards is very simple, right?
• 8:56
  Just three lines, but a real one can have several pages long in knowing which part of the game.
• 9:03
  What has changed is valuable. Then we use the game to use a game move again.
• 9:11
  This is a natural way of showing things. Again, we see the new states of the game boards and we finish the game using the linear roof.
• 9:21
  This is like a powerful move seen using linear arithmetic.
• 9:25
  Linear asymmetric here means you can apply sensitivity, commutativity, distributive, all the usual rules.
• 9:33
  This is like a big move. Is there some many things behind the scenes and you finish the game?
• 9:39
  Is least telling you you won. No ghosts should solve it anymore.
• 9:45
  Uh, and it's not just interactive game to many people.
• 9:49
  It's also an objective game. Right? Uh, I think this is one of, uh, Kevin's students.
• 9:55
  I mean, when quantum Magazine first, the first wrote the first article about learning the interview,
• 10:01
  many people from the link community and they loved this quote.
• 10:05
  She was saying that she could do 14 hours a day. Never gets tired feeling a whole day.
• 10:11
  I was really happy. This is a game that people are addicted to.
• 10:15
  It's, uh. And therefore it's unbelievable.
• 10:21
  Now, is is a cooperative project.
• 10:25
  The library has contributions from more than 500 people in more than 1.8 million lines of code.
• 10:33
  Right. And this is the actual I was talking about in the previous slides.
• 10:37
  Uh, another quote I love is for had their Macbeth because it's really captures the spirits of the community.
• 10:47
  This building something because you believe someone you.
• 10:51
  This is the foundation for someone to build something bigger.
• 10:55
  And, uh, at the time felt like, uh, what?
• 10:59
  You're going to build on top of them.
• 11:01
  I couldn't imagine how many projects would have math as the foundation, not just in maths, but also in computer science.
• 11:11
  I'm going to tell a story about mathematics, a few about software.
• 11:15
  And that very shocked one about I, Kevin, is going to tell you way more about AI during his talk.
• 11:23
  Let's focus on mathematics first. Is impossible to talk about when you start talking about the effect on space projects that caffeine.
• 11:33
  Uh, Pets.com. I saw your homecoming cheer in 19 2019.
• 11:39
  This is the project that's brought a lot of attention to this system,
• 11:43
  because they formalise its model and the mathematics they showed that it was Lee was not even capable of doing formal math, uh, advanced mathematics.
• 11:54
  But also they learned that is also which communicates after how you formalise a mathematical object in a computer.
• 12:03
  Math is data. Data that can be processed, said transform.
• 12:07
  It's inspected in many different ways.
• 12:11
  Uh, for example, the graph, this dependency graph on the left hand side was automatically generated from the perfect part space definition.
• 12:22
  Patrick Muscle wrote a program that strikes all the dependencies and builds this dependency graph for us, right?
• 12:29
  You can visualise it dependencies because math is data.
• 12:33
  Now if you go to Math Overflow, the second most upvoted question answer for the question what?
• 12:41
  What? Our effect on spaces is a link to the link definition.
• 12:45
  And the cool thing here is that basic point spaces are really complex mathematical objects.
• 12:51
  But now that they have been formalised, if you have the patience you can understand, you can keep following the dependencies.
• 12:59
  For example, here you can see that it uses something called a Tate's rank.
• 13:04
  I don't know what that each ring is. You can click and ask to see some.
• 13:08
  Show me the definition of data ring. In theory, you do it for you.
• 13:13
  Let's see how this works in practice. This is one file from F from ring theory.
• 13:19
  The first thing you can click it anywhere in your proof it to show you the state of the game.
• 13:25
  But that's that's points right? In the game.
• 13:30
  What is not a static object is interactive.
• 13:33
  You can hover over for example, and Prime is going to sesame.
• 13:37
  Prime is a submodule is gives you information about the objects.
• 13:42
  You can jump to the definition of submodule. Right.
• 13:46
  Ellie will show you the definition and you can keep doing that.
• 13:49
  You can ask what is an additive symbol? Monoids.
• 13:52
  It will show you the definition. You can keep zooming in, zoom in to your back to the axioms of mathematics.
• 14:00
  Right. You can see objects. You can change the definitions and see the impacts when you change its interactive objects.
• 14:09
  Now. Then, after the success of the specific points spaces came the challenge from the show that he is the person that came up with this concept said,
• 14:20
  okay, you have my definition now. I have these results that I'm sure about the correctness.
• 14:26
  I didn't publish it because I'm not sure I challenge you to formalise it.
• 14:32
  And he's at the time he said, I'm going obsessed about this proof.
• 14:37
  I remember Kevin approached me saying, we are going to do it.
• 14:40
  We don't know how long it's going to take, but we are going to do it anyway.
• 14:44
  Uh, at the time, felt like two years, maybe would take two years to do its.
• 14:51
  But in a few months, the main critical results that shows it wasn't sure about has been formalised by a group of people led by your coming.
• 15:03
  The cool thing is, like people working together.
• 15:08
  With the assistance of a computer. We could do it.
• 15:12
  And, uh, shows. He was very pleased. Many small mistakes were cuts during the process.
• 15:18
  The results appear on nature. Uh, is really unusual for maths to show up on nature, on the nature magazine.
• 15:27
  It didn't stop there. In my points of view. What was really unbelievable, said the Jew, not only formalised the results.
• 15:37
  They also managed to simplify the proof. Without fully understanding the proof.
• 15:43
  Because there was a computer assistance there. Uh, Yoho was telling me that he could see only two moves ahead in this game.
• 15:52
  Basically. Without being able to see the game, boys would not be able to do it.
• 15:58
  Lee was serving as a guide them right in this quote from the show that I think was one of the happiest days of my life.
• 16:07
  When I read, I feel that GDP, they really wrote that.
• 16:10
  Kevin said yes. Was that you wrote that since that meeting was really an assistance through the thick jungle?
• 16:16
  The proof is right. And he couldn't keep all the objects in his memory.
• 16:22
  Uh, his mind's rights in having computer systems allow him go beyond his native ability,
• 16:31
  so allows people to simplify a proof without fully understanding it.
• 16:35
  Uh, I think this was really remarkable.
• 16:41
  Was this was only the beginning that many other projects using link.
• 16:44
  Kevin will tell you about the Families Theorem project today that Collison projects wrong about four years of doing.
• 16:53
  Uh, also a big issue that was the questionable tum's project by to install that was completed.
• 16:58
  And Reggie. But I want to tell you about, uh.
• 17:04
  A new experiments that we have done a few weeks ago.
• 17:09
  Uh, King Morrison has been.
• 17:13
  He's such these such using link like ten years ago.
• 17:16
  Right. Was one of the first uses. Right?
• 17:19
  He was, uh, I remember when Kim started using link, they told me, oh, I want to formalise quantum computing, right.
• 17:27
  He was they were working with quantum, the quantum computing team.
• 17:32
  Uh, they wanted to formalise quantum.
• 17:35
  And many years later, now we are colleagues, we work together, and we finally manage to verify many results from a paper.
• 17:46
  Kim wrote about quantum algebras. Right? This is one of them.
• 17:51
  Rights is fully automatic, right? With one move, I'm showing you a new move called Grind Plus ring.
• 17:58
  You can do this computation automatically in milliseconds, right?
• 18:03
  This is not a toy, right? This encodes real bright constraint.
• 18:08
  How are relation by constraints deriving from relations among the diagrams in a pivotal tensor category?
• 18:15
  Writes everything in milliseconds. Uh, the main point here is that we are leaving now.
• 18:24
  You can explore new mathematical and physical structures, from topological quantum fields to fusion categories.
• 18:31
  Right. Everything automatic. You don't need to do these calculations by hand.
• 18:35
  This is another example from the paper. You see the conclusion that is a polynomial of degree 16.
• 18:41
  Imagine doing these calculations by hands. Or the one option subsumed by, hence no other option using an unverified computer.
• 18:49
  How is your brother in the fields? Always uneasy to publish a paper when you use its unverified system to check the results and range?
• 18:59
  Plus ring is just another move in the game. Writes.
• 19:06
  We're talking about all these moves in this game, but should we trust?
• 19:10
  I just mentioned that computer algebra systems are unverified, but what about Lean Leans?
• 19:17
  A vast, uh, piece of software, right?
• 19:21
  It has many bugs, but. Link has bugs.
• 19:26
  The moves can have bugs, but the chrono, it's small.
• 19:30
  It's the one that checks the proofs. The certificates that are created by this game moves that I have been showing you.
• 19:37
  But then you can say, well, the Colonel is small, but it may still have bugs.
• 19:43
  Yes, this is right. The Colonel one has. Sometimes we find bugs in the Colonel.
• 19:49
  But you can export your proofs rights and you can use external checkers.
• 19:55
  You can use external checkers to validate any proof constructed using.
• 20:01
  You can inspect. Remember, math is data. Now you can expect.
• 20:06
  You can even implement your own checker if you want.
• 20:09
  Absolute assurance. We never found a bug where all external checkers would say yes, it has been verified.
• 20:18
  It's very unlikely. That's all verified is all external checkers have the same bug, right?
• 20:24
  This gives you a lot of assurance. What did you learn?
• 20:29
  Right? We learned that machine checkable proofs enable a new level of collaboration.
• 20:35
  Many people. That's why it's all these projects. Just liquid tension experiments.
• 20:40
  They never had mats. Right. You mentioned, uh, working, I'm afraid.
• 20:45
  Usually in mathematics, you work with a small team to three people that know each other really well.
• 20:52
  Here you have people working together that they never met.
• 20:55
  Right. Is the power of the community. People are managed to formalise the results very quickly because they were.
• 21:01
  It was a bunch of people working together. You had an architect like you once set up all the interfaces, all the holes that need to be filled.
• 21:10
  But now people could work concurrently filling these holes, right?
• 21:16
  You don't need to trust automation that moves. People can ask the home moves for the game.
• 21:22
  Lee's extensible game writes. You don't need to trust the Colonel will catch mistakes you made when you implement your own moves.
• 21:32
  And the final lesson is not just about proving some, but understanding objects that are beyond your cognitive abilities, right?
• 21:41
  I think that's another big lesson we learned.
• 21:45
  Another feels like because math is data, we can do something that is done in computer science, in software developments, automatic refactoring.
• 21:55
  I have this quote here from Sulit. It is a channel.
• 21:59
  When the community join, it's like a forum where everybody exchanged messages and it's very popular.
• 22:05
  Many members of the link community are there,
• 22:08
  and they love this quote from Ricardo Brusca where he says that the result was automatically generalised.
• 22:15
  And he points out. Imagine if it was an informal paper.
• 22:20
  Someone generalises our results on a paper that was published 50 years ago.
• 22:27
  Who is going to make the propagate? Who's going to propagates this generalisation through old papers that depend on these results?
• 22:34
  Nobody. But if math now has been formalises, this happens with a push of a button, right?
• 22:42
  Software Lenovo is using mainly software verification projects rights.
• 22:48
  Each is a programming language. You can write codes and you can verify it simultaneously.
• 22:55
  You don't need to use two different language. You use the same system, right?
• 22:59
  You can prove that your code has the properties you expect.
• 23:04
  Just this quote from Mike Dykstra captures this idea very precisely.
• 23:10
  Testing can only show the presence of the bugs, not the absence.
• 23:16
  Right? See the exact exact language.
• 23:20
  Amazon Web Services is a policy language.
• 23:23
  It specifies who can access resources while its users use this language, and they create a model of GS language in length.
• 23:34
  Right? The model is open source. Anybody can use the model.
• 23:37
  Player IDs is available online. How does it work?
• 23:44
  Basically, they have the actual implementation that is in production is written in rust.
• 23:51
  And you have the model returning link. Right? In the proof, many properties about the model and they run a battery of tests.
• 24:02
  They call differential testing. They want to check if the model and the actual implementation agree on every single input.
• 24:11
  If there is a discrepancy,
• 24:13
  there is a mismatch because there is a bug in the code or the model does not capture reality and people have to go there and fix it.
• 24:24
  Why linguist not used, uh in production here, right?
• 24:29
  It will happen. The one day does not happen today because for example fast service.
• 24:35
  See, that is part of a service that people that have to be on call.
• 24:40
  If there is an issue to be able to fix the software.
• 24:43
  Right. And today we do not have link is not as popular as rust.
• 24:48
  We don't have as many developers as, uh, rust, the lean developers, as rust developers.
• 24:54
  But one day this will happen.
• 24:58
  If you want to learn more about lean, you can see the blog posts that my colleagues Kesha and the Minotaur like wrote about.
• 25:05
  See there how lean was used. Uh, they were very pleased with the performance of this system.
• 25:12
  Another example is differential privacy. Differential privacy is a mathematical framework that ensures.
• 25:21
  I mean, let's walk back a little bit why people need that.
• 25:25
  Corporations want to collect data, but they want to respect your privacy when they do that.
• 25:32
  One technique they use to add noise to the data, to make sure that nobody can figure out who this data is from,
• 25:41
  but if you add too much noise, the data is useless.
• 25:45
  If you actually know sensitive information can leak, right?
• 25:50
  And interfacial privacy, you're going to have pieces of software like a discrete Gaussian sampler, right?
• 25:58
  Used to calibrate the noise. The amount of noise in the data.
• 26:03
  And these are projects led by Jean-Baptiste Tristan at AWS.
• 26:07
  It's an open source library. You can also see the link code for this library.
• 26:12
  And one thing that I found interesting is that it not only proves correct, the simpler correct.
• 26:20
  He found bugs in the original implementation in the paper.
• 26:23
  The original implementation was based on uh, and he managed to make it twice as fast.
• 26:30
  Right. And why he just managed that?
• 26:33
  Because he could implement optimisations without the fear of introducing bugs.
• 26:41
  And Simpsons would not exist without Matlab.
• 26:45
  Well, since it relies heavily on Matlab.
• 26:48
  It uses concepts from free analysis, number theory, topology, and I remember when Jean-Baptiste mention his projects or all the math lib channel.
• 27:01
  Uh, people were shortcuts. That's math.
• 27:04
  Lib was useful for software, right? And this is not an exception.
• 27:09
  This is not the only project that relies on lib.
• 27:12
  The next one from Microsoft I Ineos right.
• 27:16
  Is this for verifying cryptography. Basically here the setup is slightly different.
• 27:22
  You have software engineering software engineers writing rust code for the crypto and uses a tool that converts rust into link.
• 27:32
  And they verified this. It's almost like is extracting the model automatically from the risk codes.
• 27:40
  And the proof engineers make sure the, uh, the proofs,
• 27:46
  the properties they once are validating the code in this model that was automatically structured.
• 27:52
  And this could only happen because of two main ingredients.
• 27:56
  They claim one is my flip. But all the number theory is essential for cryptography is they have a math leap.
• 28:03
  And the second thing link is extensible. They could edit their own moves to the game.
• 28:10
  Uh. Yeah. They, they're going through some publishing these results, which is very new, uh, in years.
• 28:18
  The two also is open source. You can use a nurse should translates rust coding to link and verify the link codes, uh, using the link proof assistance.
• 28:29
  Another example is the CLR writes. This is basically the implementation of the kernel functions.
• 28:37
  They give you a precise semantics for the kernel functions and the machine learning kernel.
• 28:43
  Right.
• 28:44
  And they also provide translation from common kernel languages implemented in Python into this one implemented singly by the code is open source.
• 28:55
  Uh, they manipulates bit vectors and fix it uh, integers.
• 29:00
  He is just showing the example where that is causing a, uh, a vector of size 64.
• 29:06
  This is a great segway for another movie in our game before he decides this is a powerful move.
• 29:13
  If he decides it's a verified beach blaster implemented by Harry moving, he's in the link fro the the non-profits responsible for developing Lean now.
• 29:24
  It's based on a verified set checker by Josh clean.
• 29:27
  He was my internet's my, uh, at, uh, Amazon in 2023.
• 29:33
  And also Siddharth and Alex from Cambridge contributed many results news to prove that the beach blaster was correct before it decides.
• 29:43
  Basically, if you had a problem in learning about bit vectors,
• 29:46
  E2 is going to use a very fine beach blaster that converts this beach vector formula into a formula in propositional logic.
• 29:55
  Then when you invoke a SAT solver that's not verified cash cow cash cow use generates a certificate that's called the L read certificates,
• 30:05
  and we have a verified check for these certificates.
• 30:09
  That is not uncommon. Should be the certificate should be 100MB long writes.
• 30:16
  Such soup is extremely fast, right? If you run for a few minutes, the SATs over.
• 30:22
  The certificate is gigantic, right? And if you decide, can check with the verify checker.
• 30:29
  Alex, use an example before deciding practice.
• 30:33
  Pop counts. Uh is a common function.
• 30:37
  You'll find many hackers use this for counting the number of bits.
• 30:43
  That's a two in a bit. Vector writes very efficiently without any loop.
• 30:48
  You just do this fancy operations with feature vectors on the left hand side, right,
• 30:53
  and it will tell you how many bits X has right through bits on their or on the rights to have this speaking length.
• 31:02
  That's you just it's just iterating counting how many bits are one.
• 31:07
  Is the standard implementation.
• 31:10
  And now we have a theorem stating that the implementation of all these funky bits vector operations actually match the pop spec, right?
• 31:22
  You have the statement of the theorem, right? Saying that the implementation match matches the specification, how the proof goes through.
• 31:31
  Basically we use the Simplifier right.
• 31:33
  To simplify is going to open all these abstractions is going to unfolds them expands them is going to expand the specification.
• 31:42
  The pop counts, the environment, the values and so on.
• 31:46
  And then Cobb decides and you can see the state of the game boards here after.
• 31:52
  Simple. This is the state of the game board on the on the right hand sides is just a bit vector problem.
• 31:59
  It's a bunch of bit vector operations of shifts, bitwise ends, addition subtraction.
• 32:06
  And now can just copy the sides and blast through it.
• 32:10
  Right. It proves that instantaneously in this case. Since we talked, uh, about bit vectors.
• 32:19
  This one. If you decide this blasting is reducing a bit vector problem into bits.
• 32:26
  But there are other strategies. Lead does not fix a specific strategy for a specific problem.
• 32:34
  For example, here you can exploit with grinds the same one which is quantum algebra.
• 32:40
  You can verify which vectors form a commutative ring.
• 32:44
  You can use the ring solver to solve this problem, right?
• 32:48
  In its most for example, we know that this ring, the ring of a bit vectors of size eight, has characteristic 256.
• 32:57
  In those, 256 is zero in this ring.
• 33:00
  Right? That's why this this property holds.
• 33:04
  You see, here is a completely different strategy. Instead of blasting things into bits, it's using the break structure.
• 33:12
  That's bits vector satisfies. And you can also use ground for example for proving that this function sift down preserves the size of the input array.
• 33:24
  This is a function for use for heap sort. All the ray access here have been verified by.
• 33:32
  This no. When linear generates code for this function, there is no runtime check for their race.
• 33:38
  The indices the each knows they're all in bounds.
• 33:41
  For example, when you say a square brackets childs, you know childs is less than the size of a.
• 33:48
  It was proven behind the scenes, and the code generator can use this fact to generate efficient codes.
• 33:56
  And the proof that this function sifts down preserves the size of the array is just a one liner.
• 34:03
  Again, a move is a powerful move that finishes the game in one line.
• 34:10
  What did we learn? Right? We learned that.
• 34:15
  For software verification. In software development, you can code without fear, right?
• 34:21
  You can implement optimisations that should before.
• 34:26
  Sometimes the person implementing or making the modification does not know all the assumptions that are needed for that to work.
• 34:35
  They know something, but they are not fully confident about the methods.
• 34:40
  You now have a proof of system to double check what you wrote.
• 34:45
  Both. Automation is essential.
• 34:47
  Link has been used in many different applications verified compilers, Polish languages, cryptography, cryptographic libraries, and so on.
• 34:55
  You can find all the projects in his effort.
• 34:58
  He's like a repository, like crates that are used for rust, where all the packages that are open source foiling are available there.
• 35:06
  You can browse them such then you know, for each version of reading each package is compatible with.
• 35:14
  And if you want to learn more how lean is using software? You can also read this blog post I wrote for Amazon.
• 35:21
  How lean is used for coding and encoding math both directions.
• 35:29
  I will be very brief here in the eye because Kevin will tell you much more.
• 35:34
  I would just, uh, tell you the obvious that large language models are amazing, but they hallucinate.
• 35:42
  It's great that for maths you can check.
• 35:45
  You can use a system like link to check if the result produced by uh, a large language models, correct or not, and just essential rights.
• 35:55
  Imagine one day large language models start proving maths like the formalised theorem automatically.
• 36:04
  The proof. The formal proofs more than 200 pages long.
• 36:09
  Would you trust? I mean the likelihoods.
• 36:12
  A life language model made a mistake in 100 pages. It's really high.
• 36:16
  But we can check now, right? Machine checkable proofs are the antidote to hallucinations in the.
• 36:26
  Uh, yeah. But the other that we talked about how lean can help I.
• 36:32
  But I can also help lean. Right. That's several groups that are building.
• 36:38
  I should predict the next move in the game and even to complete the game.
• 36:44
  You say try to help me. They will try to synthesise a proof for the whole game for you.
• 36:51
  Mean, dojo is a popular package from Caltech.
• 36:54
  It's great because everything's open source. The model, the data sets, the code.
• 37:00
  Everything's open. Right? Uh.
• 37:04
  There are also projects by OpenAI and methi where they solved some Olympiad problems in 2000.
• 37:10
  2 in 2020. 2022 2023.
• 37:15
  But the big news there was alpha proof last year.
• 37:20
  Offer proof is in the AI built by DeepMind's. Being something that's many people in the community.
• 37:27
  Effort was impossible to build a system that can get a silver medal in the animal rights.
• 37:33
  It's weeks before they announce these results.
• 37:38
  People in the community are saying, oh, this is going to take years. You will never happen.
• 37:41
  It's impossible. But now DeepMind has alpha proof that you could do it.
• 37:48
  Do you mean proofs? Right? That's machine checkable, right?
• 37:53
  Gives you absolute assurance about the correctness of the results.
• 37:59
  Well, the lessons here, I think. I'm sure you have many more.
• 38:05
  But one big issue here is that machine checkable proofs allow us to build a AI that does not hallucinates,
• 38:11
  writes AI gets better and better at understanding explaining link codes.
• 38:17
  For example to install. When he learned something, he said that he has such pitchy on his sides.
• 38:25
  He was asking questions and he learned link.
• 38:29
  With the help of ChatGPT, you can give a big link file.
• 38:33
  It will explain you in natural language what the file does right.
• 38:38
  It will help you. Okay. If you ask about this, what this move does, it will give you a really good explanation.
• 38:46
  Now in the future, for sure, we are going to have AI systems that can prove hotter than gas.
• 38:53
  Before we wrap up, I want to emphasise that's one thing that we talked a lot about machine checkable proofs.
• 39:04
  But another ingredient that enables decentralised collaboration in learning is the fact that learning is extensible.
• 39:12
  It turns out that link is implemented in link itself.
• 39:16
  Is a programming language. You can make sure. All right, the mathematicians, the Mathlete community, all the time, they change things themselves.
• 39:26
  They add their own moves. They make modifications to the system.
• 39:30
  They adds the whole new syntax. That's great for for maths.
• 39:36
  And the main point is that even if you make a mistake in a move, it doesn't matter.
• 39:42
  The kernel will catch its it. Making the system extensible I think was really important.
• 39:49
  Before the fraud this non-profit's falling. It started in 2000 2023.
• 39:56
  Sorry, ten years after we started the project would impossible to get through 2023 if lean was not extensible.
• 40:04
  There was no team right building link. And he remember the Leia riff that she mentioned at the beginning?
• 40:14
  Actually, this is a move. This was implemented by the math community.
• 40:19
  Easing side of math. Liberty's move was not implemented.
• 40:24
  I did not implemented. This move was implemented by their linked users.
• 40:30
  It's inside of math flip bifida site and Grimes just moves were also implemented jingling.
• 40:37
  You can see the code for link. You can see the code and say, oh, this doesn't do exactly what I want.
• 40:43
  I want you to do more. You can modify its.
• 40:48
  I know the fees. That link got very popular in the I because it's very easy to shoot prospects inside of Lynn.
• 40:58
  You can access Memphis data. It's okay when you formalising Lynn.
• 41:04
  Math becomes data that can be processed. But how do you access this data?
• 41:09
  You don't need any new programming language. You can use lead self truth prospecting side of the data.
• 41:17
  You can you can write a link function that traverses your proof objects.
• 41:23
  The dependency graph was built this way. Kim Boyce on the same one of the quantum uh,
• 41:29
  I was your breaks example wrote a tool for extracting data in usage by open AI method to extract data from leaf for training.
• 41:40
  The same idea of Introspecting only objects can be used to build animations.
• 41:45
  If you go to YouTube search for proof animation link, you are going to find many of these animations that were built using a two.
• 41:53
  But David's Renshaw rice if you will, for the solutions that DeepMind phones for the I am what they handy methods we're using this tool.
• 42:06
  The Leaf Frog is a non-profit that's started, uh, in 2023.
• 42:13
  Has 19 members. Now unto me being possible to run the lean projects without support of this foundation.
• 42:22
  The mission is to prove the scalability, usability, documentation, proof automation and reach self-sustainability in five years.
• 42:30
  Well, really grateful for the support from the Simmons Foundation, the Sloan Foundation, Research Working, and Alex Core.
• 42:39
  It would be impossible to do it without the support.
• 42:43
  There are too many users now asking too many things in that user.
• 42:49
  People that want to use me for teaching that's want.
• 42:52
  They have a high bar or own usability they want to use with undergraduate students, high school students that people that she wants better manuals,
• 43:01
  people that she wants more scalability, people that she wants cheese wants that without a team is impossible.
• 43:10
  These non profits also do not happen without conversions.
• 43:15
  Research conversions came up with a new concept called the Far rule Focus Research Organisation.
• 43:23
  They compare her role to something like the James Webb Telescope or some A projects that she's too big for academia and not profitable for industry.
• 43:36
  There's no profitability path for the projects,
• 43:39
  the many projects like that and conversion to support this kind of projects in help raising money and running the nonprofits.
• 43:49
  So without the support is a lot of work I didn't know before. It's a lot of work would be impossible without the help of convergence research.
• 43:59
  Live show by the numbers. Uh. Before the live show, we would have a [INAUDIBLE].
• 44:04
  It would take a long time for each release. Right now, since the fro started two years ago.
• 44:11
  Almost three years ago, we had 19 releases, more than 4000 requests with bugfixes, new features, performance improvements, and so on.
• 44:21
  All the roadmap, our roadmaps are all publicly available.
• 44:26
  Since then, link appears three times in the New York Times, Quantum Magazine, several times Scientific American, and so on.
• 44:36
  The growth of the project also accelerated.
• 44:39
  If you such, we can count easily the number of projects using lean on GitHub that more than 4000.
• 44:45
  And then you see we can see the acceleration after the we started.
• 44:51
  The number of downloads from the Visual Studio Code plugin.
• 44:55
  We have data in the Visual Studio, but. Codes.
• 44:58
  Marketplace provides data, but the data starts in 2024.
• 45:03
  You can see there were more than 40,000 installations, new installations, not updates since 2024.
• 45:13
  How can you contribute to the project? There are many different ways you can contribute.
• 45:17
  You can help using math Lib right, is that you can join the sleep channel where the community gathers.
• 45:25
  If you have questions about link, your question is going to be answered in minutes there.
• 45:31
  If you are interested in machine learning kernels, you can contribute to class projects.
• 45:36
  If you want to participate in a big formalisation project.
• 45:40
  Maths projects. You can contribute to the Families Theorem formalisation project that Kevin is running.
• 45:47
  You can create your own your projects rights and you'll be indexed automatically by his envoy.
• 45:53
  If you host it on on GitHub, you can use link without installing anything.
• 46:00
  You can go to Life bottling link.org/using link please.
• 46:05
  It's math lib everything in your browser.
• 46:09
  You can also support the nonprofits, not just by providing funding and partnerships, but also for creating for the projects.
• 46:18
  It's super helpful for us. Advocacy is really important.
• 46:24
  Uh. Uh, I'm very happy to be here today.
• 46:28
  The message I want to communicate is that learning is an efficient programming language and proof assistance.
• 46:33
  The Muslim community is changing how math is done. It's not just about proving, but going beyond your cognitive abilities.
• 46:41
  Right. In the future, we are going to have AI that's will be an assistant to you.
• 46:47
  You're going to have big projects, solving hard problems once people that you never have met, and even the AI, everybody working together, right?
• 46:56
  Lee will track the details. Right? Centralised collaboration allowed large teams to work together.
• 47:05
  You don't need to take the result of someone on faith anymore.
• 47:09
  Thank you very much.