1 00:00:01,040 --> 00:00:05,310 [Auto-generated transcript. Edits may have been applied for clarity.] So if you haven't. 2 00:00:15,080 --> 00:00:19,069 Okay. So welcome everybody to the day. So straight to lecture. 3 00:00:19,070 --> 00:00:26,030 So this is uh two distinguished lectures which are named after Christopher Straight genius who founded the programming research group here. 4 00:00:26,690 --> 00:00:31,999 And this is a particularly exciting lecture, uh, because we've got two lectures, 5 00:00:32,000 --> 00:00:36,980 both we had tomorrow and Kevin Bussard and, in my opinion, talking about it. 6 00:00:37,370 --> 00:00:45,290 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. 7 00:00:45,300 --> 00:00:48,980 So we're really, um, very, very happy to have them here. 8 00:00:49,640 --> 00:00:57,380 Um, so before I introduce the speakers, I want to thank, um, Oxford Asset Management, who's been funding the series since 2015. 9 00:00:57,950 --> 00:01:04,700 And we're really grateful for their support because, um, we get such amazing speakers, uh, thanks to them. 10 00:01:05,120 --> 00:01:11,600 And for any students and researchers that want to find out more about their company, you can do that after the second talk. 11 00:01:11,840 --> 00:01:19,580 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. 12 00:01:20,060 --> 00:01:24,470 Then we're going to have questions and answers, and there will be a microphone going around. 13 00:01:24,860 --> 00:01:27,860 And then we'll have the same thing. Um, for Kevin. 14 00:01:28,970 --> 00:01:29,450 Okay. 15 00:01:29,540 --> 00:01:39,200 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. 16 00:01:39,650 --> 00:01:46,010 Um, he's currently, uh, I can read it off, a senior principal applied scientist at MIT. 17 00:01:46,340 --> 00:01:50,300 And before that, he had a, um, a similar role at Microsoft. 18 00:01:50,840 --> 00:01:58,070 Now, actually, he's not only the person who, um, built the limit theorem prover, but actually lots of other theorem provers, too. 19 00:01:58,820 --> 00:02:03,500 And I was not here a list of, um, prizes for such work. 20 00:02:03,950 --> 00:02:15,480 Um, so he received the award in 2021 for pioneering contributions to the foundations of the theory and practice of satisfiability modulo theory. 21 00:02:16,430 --> 00:02:23,870 The high for Verification Conference award in 2010 for the most influential work in the last five years in verification, 22 00:02:24,380 --> 00:02:28,100 the Herb Brent Award for Distinguished Contributions to Automated Reasoning. 23 00:02:28,100 --> 00:02:35,600 That was in 2019, the Programming Language of Software Award of the ACM in 2015 for the Z3 theorem prover. 24 00:02:35,600 --> 00:02:36,980 So that's another theorem prover. 25 00:02:37,460 --> 00:02:45,920 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. 26 00:02:45,920 --> 00:02:50,300 And I said, thank you, thank you, thank you for such a kind introduction. 27 00:02:57,600 --> 00:03:04,230 Thank you very much. Uh, very happy to be here. And it's a pleasure to be here giving a talk with Kevin today. 28 00:03:05,040 --> 00:03:15,200 I want to tell you about Linc. Uh, that means whatever the reason, motivation for Linc was, uh, software verification, right? 29 00:03:15,300 --> 00:03:20,129 I mean, Z3 was very popular. It's bug finding bug finance. 30 00:03:20,130 --> 00:03:27,600 Microsoft was very influential there, but the goal was, can we make the same having the same success of such verification? 31 00:03:28,290 --> 00:03:34,740 We went through a very strange path from the heavy impacting mathematics that we never had dream of. 32 00:03:35,700 --> 00:03:43,610 Uh, but the goal. In both cases, it's like we both software. 33 00:03:44,680 --> 00:03:48,430 Mathematics in AI. Should they rely on manual review? 34 00:03:48,640 --> 00:03:56,110 Partial testing. I'm stating the theorem can be catastrophic or invalidates the whole results. 35 00:03:56,320 --> 00:03:59,410 Same thing for critical piece of software. Right. 36 00:03:59,560 --> 00:04:04,390 And one thing I see all the time, people fearing to make a change, 37 00:04:04,420 --> 00:04:10,750 a piece of software because they fear by making the change they may be introducing a bug. 38 00:04:10,990 --> 00:04:17,440 Especially if it's a critical piece of software. Uh, until you have machine checkable proofs. 39 00:04:17,650 --> 00:04:23,180 Right? You cannot. You don't need to check them only offline, but with also external checkers. 40 00:04:23,200 --> 00:04:27,160 And this of completely avoids the guesswork, right? 41 00:04:27,260 --> 00:04:32,200 You you create trusts. You have absolute trust now that your result is correct. 42 00:04:32,890 --> 00:04:36,070 And there are many consequences that we didn't expect. 43 00:04:36,520 --> 00:04:40,960 Like, it's not just about proving but about collaboration. 44 00:04:41,170 --> 00:04:49,840 And that's one of the messages we want to communicate today. These are open source programming language improv assistance. 45 00:04:50,140 --> 00:04:58,030 Right? Uh, and, I mean, we couldn't bring the impact he's having in mathematics software verification. 46 00:04:58,030 --> 00:05:01,810 I the project starting 2014, right. 47 00:05:02,110 --> 00:05:06,370 The goal at the time was to combine the automated interactive worlds. 48 00:05:06,940 --> 00:05:12,820 Uh, they're both called that three and linear are both called two improvers, but they are completely different beasts. 49 00:05:13,420 --> 00:05:17,830 Right. And the main thing is, are the machine checkable proofs. 50 00:05:18,460 --> 00:05:23,140 We say this eliminates the trust bottleneck, not a trust between humans. 51 00:05:23,140 --> 00:05:31,090 But now the trust between humans and machines AIS right in it opens up new possibilities for collaboration. 52 00:05:32,320 --> 00:05:35,500 Let's see an example here how link looks like this. 53 00:05:35,500 --> 00:05:40,000 If you substitute your codes, I think the community. This is the favourite edge story. 54 00:05:40,000 --> 00:05:49,329 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. 55 00:05:49,330 --> 00:05:56,050 Very simple one. In lean you have libraries. Here we are importing math lib, the lean mathematical library. 56 00:05:57,100 --> 00:06:00,700 We have definitions. Definitions have names. It's called ODS. 57 00:06:00,700 --> 00:06:05,050 Here it states in this in a natural number these odds number. 58 00:06:05,350 --> 00:06:11,410 If there is a k such that's n equals two times k plus one writes the usual definition. 59 00:06:12,520 --> 00:06:16,450 Now that you have a definition, you can write theorems about this definition. 60 00:06:17,050 --> 00:06:24,850 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. 61 00:06:25,930 --> 00:06:29,559 After you made a claim you can start trying to prove this is a proof. 62 00:06:29,560 --> 00:06:36,610 You're saying that's key is true. And link accepts it as a valid proof because five is two times two plus one. 63 00:06:37,000 --> 00:06:42,729 This is a proof that that's five sides a number. If you give an invalid proof link will complain. 64 00:06:42,730 --> 00:06:50,520 We are going to get a squiggly line. Now let's try to prove something more complicated is to make a point. 65 00:06:51,120 --> 00:06:54,360 That's leaves interactive again. I was very happy. 66 00:06:54,600 --> 00:07:03,870 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. 67 00:07:03,870 --> 00:07:11,100 Computer game. And I was actually super happy when as a teenager, I loved to implement computer games. 68 00:07:11,400 --> 00:07:17,550 I never meant for my games when I was a teenager who were played by anybody but by myself. 69 00:07:17,760 --> 00:07:22,470 And now I found I finally built a game that had real users rights. 70 00:07:23,280 --> 00:07:28,380 And here on the right hand side, this is the board of the game. 71 00:07:28,980 --> 00:07:34,680 This is this. Like when you are playing chess, you have this state of the chess boards here. 72 00:07:34,680 --> 00:07:39,390 The right hand side is the board game. Let's see. 73 00:07:39,960 --> 00:07:43,280 We are going to start. The first move of this game is intro. 74 00:07:43,390 --> 00:07:50,310 We are trying to prove that if a number and odds this square is odds two, you're going to do introduction. 75 00:07:50,850 --> 00:07:55,530 We are giving name if n is item number these are k. We're giving a name k1. 76 00:07:56,820 --> 00:08:08,850 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. 77 00:08:09,300 --> 00:08:13,860 And we give a name here in one we can give names to hypothesis. 78 00:08:15,030 --> 00:08:18,899 Then we use the most popular move in the game. 79 00:08:18,900 --> 00:08:29,070 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. 80 00:08:29,370 --> 00:08:32,400 Need to apply simplification rules. 81 00:08:32,420 --> 00:08:41,640 Stirling. Also in the square brackets use E1B square telling you replace m by two times k1 plus one. 82 00:08:41,940 --> 00:08:47,549 You're also telling me intro expansion the definition of odds and number in ling. 83 00:08:47,550 --> 00:08:56,200 Maxine Greene. The part of the game board that has been modified in this game boards is very simple, right? 84 00:08:56,250 --> 00:09:03,569 Just three lines, but a real one can have several pages long in knowing which part of the game. 85 00:09:03,570 --> 00:09:10,660 What has changed is valuable. Then we use the game to use a game move again. 86 00:09:11,350 --> 00:09:21,520 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. 87 00:09:21,970 --> 00:09:25,690 This is like a powerful move seen using linear arithmetic. 88 00:09:25,990 --> 00:09:33,070 Linear asymmetric here means you can apply sensitivity, commutativity, distributive, all the usual rules. 89 00:09:33,580 --> 00:09:39,220 This is like a big move. Is there some many things behind the scenes and you finish the game? 90 00:09:39,290 --> 00:09:43,360 Is least telling you you won. No ghosts should solve it anymore. 91 00:09:45,530 --> 00:09:49,909 Uh, and it's not just interactive game to many people. 92 00:09:49,910 --> 00:09:55,340 It's also an objective game. Right? Uh, I think this is one of, uh, Kevin's students. 93 00:09:55,340 --> 00:10:01,100 I mean, when quantum Magazine first, the first wrote the first article about learning the interview, 94 00:10:01,100 --> 00:10:04,910 many people from the link community and they loved this quote. 95 00:10:05,090 --> 00:10:11,210 She was saying that she could do 14 hours a day. Never gets tired feeling a whole day. 96 00:10:11,510 --> 00:10:15,379 I was really happy. This is a game that people are addicted to. 97 00:10:15,380 --> 00:10:21,410 It's, uh. And therefore it's unbelievable. 98 00:10:21,460 --> 00:10:24,710 Now, is is a cooperative project. 99 00:10:25,070 --> 00:10:32,660 The library has contributions from more than 500 people in more than 1.8 million lines of code. 100 00:10:33,140 --> 00:10:37,790 Right. And this is the actual I was talking about in the previous slides. 101 00:10:37,790 --> 00:10:46,820 Uh, another quote I love is for had their Macbeth because it's really captures the spirits of the community. 102 00:10:47,150 --> 00:10:51,560 This building something because you believe someone you. 103 00:10:51,570 --> 00:10:55,010 This is the foundation for someone to build something bigger. 104 00:10:55,640 --> 00:10:59,880 And, uh, at the time felt like, uh, what? 105 00:10:59,900 --> 00:11:00,980 You're going to build on top of them. 106 00:11:01,030 --> 00:11:10,130 I couldn't imagine how many projects would have math as the foundation, not just in maths, but also in computer science. 107 00:11:11,150 --> 00:11:15,380 I'm going to tell a story about mathematics, a few about software. 108 00:11:15,830 --> 00:11:21,620 And that very shocked one about I, Kevin, is going to tell you way more about AI during his talk. 109 00:11:23,120 --> 00:11:32,600 Let's focus on mathematics first. Is impossible to talk about when you start talking about the effect on space projects that caffeine. 110 00:11:33,340 --> 00:11:39,080 Uh, Pets.com. I saw your homecoming cheer in 19 2019. 111 00:11:39,860 --> 00:11:43,160 This is the project that's brought a lot of attention to this system, 112 00:11:43,490 --> 00:11:53,660 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. 113 00:11:54,170 --> 00:12:02,750 But also they learned that is also which communicates after how you formalise a mathematical object in a computer. 114 00:12:03,320 --> 00:12:07,670 Math is data. Data that can be processed, said transform. 115 00:12:07,680 --> 00:12:09,980 It's inspected in many different ways. 116 00:12:11,660 --> 00:12:22,130 Uh, for example, the graph, this dependency graph on the left hand side was automatically generated from the perfect part space definition. 117 00:12:22,970 --> 00:12:29,870 Patrick Muscle wrote a program that strikes all the dependencies and builds this dependency graph for us, right? 118 00:12:29,870 --> 00:12:33,559 You can visualise it dependencies because math is data. 119 00:12:33,560 --> 00:12:41,210 Now if you go to Math Overflow, the second most upvoted question answer for the question what? 120 00:12:41,290 --> 00:12:44,900 What? Our effect on spaces is a link to the link definition. 121 00:12:45,680 --> 00:12:51,470 And the cool thing here is that basic point spaces are really complex mathematical objects. 122 00:12:51,920 --> 00:12:59,450 But now that they have been formalised, if you have the patience you can understand, you can keep following the dependencies. 123 00:12:59,990 --> 00:13:04,100 For example, here you can see that it uses something called a Tate's rank. 124 00:13:04,460 --> 00:13:08,450 I don't know what that each ring is. You can click and ask to see some. 125 00:13:08,470 --> 00:13:12,230 Show me the definition of data ring. In theory, you do it for you. 126 00:13:13,130 --> 00:13:18,530 Let's see how this works in practice. This is one file from F from ring theory. 127 00:13:19,670 --> 00:13:25,700 The first thing you can click it anywhere in your proof it to show you the state of the game. 128 00:13:25,700 --> 00:13:30,109 But that's that's points right? In the game. 129 00:13:30,110 --> 00:13:33,140 What is not a static object is interactive. 130 00:13:33,170 --> 00:13:37,340 You can hover over for example, and Prime is going to sesame. 131 00:13:37,340 --> 00:13:41,840 Prime is a submodule is gives you information about the objects. 132 00:13:42,290 --> 00:13:45,830 You can jump to the definition of submodule. Right. 133 00:13:46,010 --> 00:13:49,249 Ellie will show you the definition and you can keep doing that. 134 00:13:49,250 --> 00:13:52,250 You can ask what is an additive symbol? Monoids. 135 00:13:52,850 --> 00:13:59,900 It will show you the definition. You can keep zooming in, zoom in to your back to the axioms of mathematics. 136 00:14:00,320 --> 00:14:09,260 Right. You can see objects. You can change the definitions and see the impacts when you change its interactive objects. 137 00:14:09,260 --> 00:14:20,140 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, 138 00:14:20,150 --> 00:14:26,140 okay, you have my definition now. I have these results that I'm sure about the correctness. 139 00:14:26,150 --> 00:14:31,490 I didn't publish it because I'm not sure I challenge you to formalise it. 140 00:14:32,690 --> 00:14:36,920 And he's at the time he said, I'm going obsessed about this proof. 141 00:14:37,730 --> 00:14:40,820 I remember Kevin approached me saying, we are going to do it. 142 00:14:40,850 --> 00:14:44,090 We don't know how long it's going to take, but we are going to do it anyway. 143 00:14:44,960 --> 00:14:50,330 Uh, at the time, felt like two years, maybe would take two years to do its. 144 00:14:51,660 --> 00:15:02,280 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. 145 00:15:03,900 --> 00:15:07,170 The cool thing is, like people working together. 146 00:15:08,140 --> 00:15:12,070 With the assistance of a computer. We could do it. 147 00:15:12,580 --> 00:15:18,040 And, uh, shows. He was very pleased. Many small mistakes were cuts during the process. 148 00:15:18,310 --> 00:15:25,810 The results appear on nature. Uh, is really unusual for maths to show up on nature, on the nature magazine. 149 00:15:27,820 --> 00:15:37,180 It didn't stop there. In my points of view. What was really unbelievable, said the Jew, not only formalised the results. 150 00:15:37,780 --> 00:15:42,550 They also managed to simplify the proof. Without fully understanding the proof. 151 00:15:43,090 --> 00:15:51,130 Because there was a computer assistance there. Uh, Yoho was telling me that he could see only two moves ahead in this game. 152 00:15:52,150 --> 00:15:58,300 Basically. Without being able to see the game, boys would not be able to do it. 153 00:15:58,420 --> 00:16:06,520 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. 154 00:16:07,060 --> 00:16:10,600 When I read, I feel that GDP, they really wrote that. 155 00:16:10,630 --> 00:16:16,930 Kevin said yes. Was that you wrote that since that meeting was really an assistance through the thick jungle? 156 00:16:16,960 --> 00:16:22,030 The proof is right. And he couldn't keep all the objects in his memory. 157 00:16:22,660 --> 00:16:31,000 Uh, his mind's rights in having computer systems allow him go beyond his native ability, 158 00:16:31,000 --> 00:16:35,380 so allows people to simplify a proof without fully understanding it. 159 00:16:35,890 --> 00:16:40,000 Uh, I think this was really remarkable. 160 00:16:41,050 --> 00:16:44,470 Was this was only the beginning that many other projects using link. 161 00:16:44,830 --> 00:16:52,970 Kevin will tell you about the Families Theorem project today that Collison projects wrong about four years of doing. 162 00:16:53,480 --> 00:16:58,570 Uh, also a big issue that was the questionable tum's project by to install that was completed. 163 00:16:58,570 --> 00:17:03,580 And Reggie. But I want to tell you about, uh. 164 00:17:04,090 --> 00:17:07,810 A new experiments that we have done a few weeks ago. 165 00:17:09,130 --> 00:17:12,250 Uh, King Morrison has been. 166 00:17:13,300 --> 00:17:16,570 He's such these such using link like ten years ago. 167 00:17:16,720 --> 00:17:19,450 Right. Was one of the first uses. Right? 168 00:17:19,540 --> 00:17:27,320 He was, uh, I remember when Kim started using link, they told me, oh, I want to formalise quantum computing, right. 169 00:17:27,340 --> 00:17:31,840 He was they were working with quantum, the quantum computing team. 170 00:17:32,020 --> 00:17:34,540 Uh, they wanted to formalise quantum. 171 00:17:35,870 --> 00:17:46,170 And many years later, now we are colleagues, we work together, and we finally manage to verify many results from a paper. 172 00:17:46,190 --> 00:17:51,560 Kim wrote about quantum algebras. Right? This is one of them. 173 00:17:51,740 --> 00:17:58,010 Rights is fully automatic, right? With one move, I'm showing you a new move called Grind Plus ring. 174 00:17:58,370 --> 00:18:03,110 You can do this computation automatically in milliseconds, right? 175 00:18:03,860 --> 00:18:08,060 This is not a toy, right? This encodes real bright constraint. 176 00:18:08,510 --> 00:18:15,440 How are relation by constraints deriving from relations among the diagrams in a pivotal tensor category? 177 00:18:15,520 --> 00:18:24,310 Writes everything in milliseconds. Uh, the main point here is that we are leaving now. 178 00:18:24,610 --> 00:18:31,130 You can explore new mathematical and physical structures, from topological quantum fields to fusion categories. 179 00:18:31,150 --> 00:18:35,020 Right. Everything automatic. You don't need to do these calculations by hand. 180 00:18:35,290 --> 00:18:40,810 This is another example from the paper. You see the conclusion that is a polynomial of degree 16. 181 00:18:41,170 --> 00:18:49,710 Imagine doing these calculations by hands. Or the one option subsumed by, hence no other option using an unverified computer. 182 00:18:49,740 --> 00:18:59,360 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? 183 00:18:59,760 --> 00:19:03,360 Plus ring is just another move in the game. Writes. 184 00:19:06,280 --> 00:19:10,300 We're talking about all these moves in this game, but should we trust? 185 00:19:10,820 --> 00:19:17,080 I just mentioned that computer algebra systems are unverified, but what about Lean Leans? 186 00:19:17,080 --> 00:19:20,740 A vast, uh, piece of software, right? 187 00:19:21,340 --> 00:19:26,180 It has many bugs, but. Link has bugs. 188 00:19:26,190 --> 00:19:30,540 The moves can have bugs, but the chrono, it's small. 189 00:19:30,570 --> 00:19:37,080 It's the one that checks the proofs. The certificates that are created by this game moves that I have been showing you. 190 00:19:37,800 --> 00:19:43,410 But then you can say, well, the Colonel is small, but it may still have bugs. 191 00:19:43,890 --> 00:19:48,630 Yes, this is right. The Colonel one has. Sometimes we find bugs in the Colonel. 192 00:19:49,350 --> 00:19:54,570 But you can export your proofs rights and you can use external checkers. 193 00:19:55,410 --> 00:20:00,460 You can use external checkers to validate any proof constructed using. 194 00:20:01,010 --> 00:20:05,580 You can inspect. Remember, math is data. Now you can expect. 195 00:20:06,000 --> 00:20:09,720 You can even implement your own checker if you want. 196 00:20:09,750 --> 00:20:17,910 Absolute assurance. We never found a bug where all external checkers would say yes, it has been verified. 197 00:20:18,450 --> 00:20:24,650 It's very unlikely. That's all verified is all external checkers have the same bug, right? 198 00:20:24,870 --> 00:20:29,800 This gives you a lot of assurance. What did you learn? 199 00:20:29,970 --> 00:20:35,340 Right? We learned that machine checkable proofs enable a new level of collaboration. 200 00:20:35,820 --> 00:20:39,990 Many people. That's why it's all these projects. Just liquid tension experiments. 201 00:20:40,290 --> 00:20:45,420 They never had mats. Right. You mentioned, uh, working, I'm afraid. 202 00:20:45,690 --> 00:20:51,930 Usually in mathematics, you work with a small team to three people that know each other really well. 203 00:20:52,180 --> 00:20:55,350 Here you have people working together that they never met. 204 00:20:55,620 --> 00:21:01,380 Right. Is the power of the community. People are managed to formalise the results very quickly because they were. 205 00:21:01,830 --> 00:21:10,470 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. 206 00:21:10,680 --> 00:21:14,790 But now people could work concurrently filling these holes, right? 207 00:21:16,290 --> 00:21:22,140 You don't need to trust automation that moves. People can ask the home moves for the game. 208 00:21:22,410 --> 00:21:31,530 Lee's extensible game writes. You don't need to trust the Colonel will catch mistakes you made when you implement your own moves. 209 00:21:32,580 --> 00:21:41,460 And the final lesson is not just about proving some, but understanding objects that are beyond your cognitive abilities, right? 210 00:21:41,580 --> 00:21:44,390 I think that's another big lesson we learned. 211 00:21:45,690 --> 00:21:54,720 Another feels like because math is data, we can do something that is done in computer science, in software developments, automatic refactoring. 212 00:21:55,440 --> 00:21:58,680 I have this quote here from Sulit. It is a channel. 213 00:21:59,010 --> 00:22:05,170 When the community join, it's like a forum where everybody exchanged messages and it's very popular. 214 00:22:05,190 --> 00:22:07,410 Many members of the link community are there, 215 00:22:08,250 --> 00:22:15,270 and they love this quote from Ricardo Brusca where he says that the result was automatically generalised. 216 00:22:15,750 --> 00:22:20,819 And he points out. Imagine if it was an informal paper. 217 00:22:20,820 --> 00:22:26,430 Someone generalises our results on a paper that was published 50 years ago. 218 00:22:27,000 --> 00:22:33,810 Who is going to make the propagate? Who's going to propagates this generalisation through old papers that depend on these results? 219 00:22:34,110 --> 00:22:40,710 Nobody. But if math now has been formalises, this happens with a push of a button, right? 220 00:22:42,720 --> 00:22:47,940 Software Lenovo is using mainly software verification projects rights. 221 00:22:48,720 --> 00:22:55,170 Each is a programming language. You can write codes and you can verify it simultaneously. 222 00:22:55,200 --> 00:22:59,310 You don't need to use two different language. You use the same system, right? 223 00:22:59,700 --> 00:23:03,420 You can prove that your code has the properties you expect. 224 00:23:04,450 --> 00:23:10,390 Just this quote from Mike Dykstra captures this idea very precisely. 225 00:23:10,750 --> 00:23:15,580 Testing can only show the presence of the bugs, not the absence. 226 00:23:16,000 --> 00:23:19,980 Right? See the exact exact language. 227 00:23:20,330 --> 00:23:23,720 Amazon Web Services is a policy language. 228 00:23:23,960 --> 00:23:33,920 It specifies who can access resources while its users use this language, and they create a model of GS language in length. 229 00:23:34,340 --> 00:23:37,640 Right? The model is open source. Anybody can use the model. 230 00:23:37,650 --> 00:23:43,150 Player IDs is available online. How does it work? 231 00:23:44,350 --> 00:23:50,290 Basically, they have the actual implementation that is in production is written in rust. 232 00:23:51,800 --> 00:24:01,790 And you have the model returning link. Right? In the proof, many properties about the model and they run a battery of tests. 233 00:24:02,150 --> 00:24:10,970 They call differential testing. They want to check if the model and the actual implementation agree on every single input. 234 00:24:11,510 --> 00:24:13,460 If there is a discrepancy, 235 00:24:13,700 --> 00:24:23,480 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. 236 00:24:24,470 --> 00:24:29,510 Why linguist not used, uh in production here, right? 237 00:24:29,660 --> 00:24:35,020 It will happen. The one day does not happen today because for example fast service. 238 00:24:35,030 --> 00:24:39,890 See, that is part of a service that people that have to be on call. 239 00:24:40,040 --> 00:24:43,519 If there is an issue to be able to fix the software. 240 00:24:43,520 --> 00:24:48,300 Right. And today we do not have link is not as popular as rust. 241 00:24:48,320 --> 00:24:54,410 We don't have as many developers as, uh, rust, the lean developers, as rust developers. 242 00:24:54,410 --> 00:24:56,180 But one day this will happen. 243 00:24:58,030 --> 00:25:05,860 If you want to learn more about lean, you can see the blog posts that my colleagues Kesha and the Minotaur like wrote about. 244 00:25:05,870 --> 00:25:11,740 See there how lean was used. Uh, they were very pleased with the performance of this system. 245 00:25:12,910 --> 00:25:21,070 Another example is differential privacy. Differential privacy is a mathematical framework that ensures. 246 00:25:21,100 --> 00:25:25,810 I mean, let's walk back a little bit why people need that. 247 00:25:25,960 --> 00:25:31,720 Corporations want to collect data, but they want to respect your privacy when they do that. 248 00:25:32,110 --> 00:25:40,330 One technique they use to add noise to the data, to make sure that nobody can figure out who this data is from, 249 00:25:41,290 --> 00:25:45,250 but if you add too much noise, the data is useless. 250 00:25:45,700 --> 00:25:50,080 If you actually know sensitive information can leak, right? 251 00:25:50,530 --> 00:25:57,730 And interfacial privacy, you're going to have pieces of software like a discrete Gaussian sampler, right? 252 00:25:58,120 --> 00:26:01,210 Used to calibrate the noise. The amount of noise in the data. 253 00:26:03,420 --> 00:26:07,080 And these are projects led by Jean-Baptiste Tristan at AWS. 254 00:26:07,290 --> 00:26:10,980 It's an open source library. You can also see the link code for this library. 255 00:26:12,460 --> 00:26:19,690 And one thing that I found interesting is that it not only proves correct, the simpler correct. 256 00:26:20,740 --> 00:26:23,830 He found bugs in the original implementation in the paper. 257 00:26:23,830 --> 00:26:29,700 The original implementation was based on uh, and he managed to make it twice as fast. 258 00:26:30,220 --> 00:26:33,520 Right. And why he just managed that? 259 00:26:33,520 --> 00:26:39,340 Because he could implement optimisations without the fear of introducing bugs. 260 00:26:41,700 --> 00:26:45,420 And Simpsons would not exist without Matlab. 261 00:26:45,870 --> 00:26:48,760 Well, since it relies heavily on Matlab. 262 00:26:48,780 --> 00:27:00,810 It uses concepts from free analysis, number theory, topology, and I remember when Jean-Baptiste mention his projects or all the math lib channel. 263 00:27:01,410 --> 00:27:04,739 Uh, people were shortcuts. That's math. 264 00:27:04,740 --> 00:27:09,000 Lib was useful for software, right? And this is not an exception. 265 00:27:09,000 --> 00:27:12,120 This is not the only project that relies on lib. 266 00:27:12,450 --> 00:27:15,990 The next one from Microsoft I Ineos right. 267 00:27:16,230 --> 00:27:22,110 Is this for verifying cryptography. Basically here the setup is slightly different. 268 00:27:22,650 --> 00:27:31,650 You have software engineering software engineers writing rust code for the crypto and uses a tool that converts rust into link. 269 00:27:32,900 --> 00:27:38,960 And they verified this. It's almost like is extracting the model automatically from the risk codes. 270 00:27:40,040 --> 00:27:46,010 And the proof engineers make sure the, uh, the proofs, 271 00:27:46,190 --> 00:27:51,530 the properties they once are validating the code in this model that was automatically structured. 272 00:27:52,370 --> 00:27:56,149 And this could only happen because of two main ingredients. 273 00:27:56,150 --> 00:28:03,620 They claim one is my flip. But all the number theory is essential for cryptography is they have a math leap. 274 00:28:03,860 --> 00:28:09,050 And the second thing link is extensible. They could edit their own moves to the game. 275 00:28:10,280 --> 00:28:18,720 Uh. Yeah. They, they're going through some publishing these results, which is very new, uh, in years. 276 00:28:18,810 --> 00:28:27,750 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. 277 00:28:29,280 --> 00:28:37,570 Another example is the CLR writes. This is basically the implementation of the kernel functions. 278 00:28:37,810 --> 00:28:43,270 They give you a precise semantics for the kernel functions and the machine learning kernel. 279 00:28:43,690 --> 00:28:43,930 Right. 280 00:28:44,080 --> 00:28:54,580 And they also provide translation from common kernel languages implemented in Python into this one implemented singly by the code is open source. 281 00:28:55,330 --> 00:29:00,340 Uh, they manipulates bit vectors and fix it uh, integers. 282 00:29:00,640 --> 00:29:05,350 He is just showing the example where that is causing a, uh, a vector of size 64. 283 00:29:06,100 --> 00:29:13,120 This is a great segway for another movie in our game before he decides this is a powerful move. 284 00:29:13,600 --> 00:29:23,380 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. 285 00:29:24,010 --> 00:29:27,520 It's based on a verified set checker by Josh clean. 286 00:29:27,970 --> 00:29:32,410 He was my internet's my, uh, at, uh, Amazon in 2023. 287 00:29:33,130 --> 00:29:43,240 And also Siddharth and Alex from Cambridge contributed many results news to prove that the beach blaster was correct before it decides. 288 00:29:43,270 --> 00:29:46,300 Basically, if you had a problem in learning about bit vectors, 289 00:29:46,990 --> 00:29:55,270 E2 is going to use a very fine beach blaster that converts this beach vector formula into a formula in propositional logic. 290 00:29:55,690 --> 00:30:05,500 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, 291 00:30:05,860 --> 00:30:09,220 and we have a verified check for these certificates. 292 00:30:09,640 --> 00:30:15,430 That is not uncommon. Should be the certificate should be 100MB long writes. 293 00:30:16,730 --> 00:30:21,920 Such soup is extremely fast, right? If you run for a few minutes, the SATs over. 294 00:30:22,280 --> 00:30:27,830 The certificate is gigantic, right? And if you decide, can check with the verify checker. 295 00:30:29,420 --> 00:30:32,480 Alex, use an example before deciding practice. 296 00:30:33,560 --> 00:30:37,610 Pop counts. Uh is a common function. 297 00:30:37,610 --> 00:30:42,680 You'll find many hackers use this for counting the number of bits. 298 00:30:43,190 --> 00:30:47,990 That's a two in a bit. Vector writes very efficiently without any loop. 299 00:30:48,500 --> 00:30:53,480 You just do this fancy operations with feature vectors on the left hand side, right, 300 00:30:53,690 --> 00:31:01,760 and it will tell you how many bits X has right through bits on their or on the rights to have this speaking length. 301 00:31:02,120 --> 00:31:07,040 That's you just it's just iterating counting how many bits are one. 302 00:31:07,070 --> 00:31:09,320 Is the standard implementation. 303 00:31:10,910 --> 00:31:21,260 And now we have a theorem stating that the implementation of all these funky bits vector operations actually match the pop spec, right? 304 00:31:22,190 --> 00:31:31,130 You have the statement of the theorem, right? Saying that the implementation match matches the specification, how the proof goes through. 305 00:31:31,580 --> 00:31:33,850 Basically we use the Simplifier right. 306 00:31:33,890 --> 00:31:42,080 To simplify is going to open all these abstractions is going to unfolds them expands them is going to expand the specification. 307 00:31:42,290 --> 00:31:45,950 The pop counts, the environment, the values and so on. 308 00:31:46,550 --> 00:31:52,760 And then Cobb decides and you can see the state of the game boards here after. 309 00:31:52,760 --> 00:31:59,030 Simple. This is the state of the game board on the on the right hand sides is just a bit vector problem. 310 00:31:59,330 --> 00:32:05,900 It's a bunch of bit vector operations of shifts, bitwise ends, addition subtraction. 311 00:32:06,740 --> 00:32:10,370 And now can just copy the sides and blast through it. 312 00:32:10,670 --> 00:32:18,830 Right. It proves that instantaneously in this case. Since we talked, uh, about bit vectors. 313 00:32:19,790 --> 00:32:25,580 This one. If you decide this blasting is reducing a bit vector problem into bits. 314 00:32:26,210 --> 00:32:33,650 But there are other strategies. Lead does not fix a specific strategy for a specific problem. 315 00:32:34,250 --> 00:32:39,770 For example, here you can exploit with grinds the same one which is quantum algebra. 316 00:32:40,310 --> 00:32:43,820 You can verify which vectors form a commutative ring. 317 00:32:44,090 --> 00:32:47,840 You can use the ring solver to solve this problem, right? 318 00:32:48,720 --> 00:32:56,480 In its most for example, we know that this ring, the ring of a bit vectors of size eight, has characteristic 256. 319 00:32:57,080 --> 00:33:00,110 In those, 256 is zero in this ring. 320 00:33:00,500 --> 00:33:03,710 Right? That's why this this property holds. 321 00:33:04,410 --> 00:33:12,680 You see, here is a completely different strategy. Instead of blasting things into bits, it's using the break structure. 322 00:33:12,950 --> 00:33:23,660 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. 323 00:33:24,350 --> 00:33:30,890 This is a function for use for heap sort. All the ray access here have been verified by. 324 00:33:32,060 --> 00:33:37,730 This no. When linear generates code for this function, there is no runtime check for their race. 325 00:33:38,180 --> 00:33:41,660 The indices the each knows they're all in bounds. 326 00:33:41,840 --> 00:33:48,410 For example, when you say a square brackets childs, you know childs is less than the size of a. 327 00:33:48,680 --> 00:33:55,760 It was proven behind the scenes, and the code generator can use this fact to generate efficient codes. 328 00:33:56,840 --> 00:34:03,320 And the proof that this function sifts down preserves the size of the array is just a one liner. 329 00:34:03,890 --> 00:34:08,270 Again, a move is a powerful move that finishes the game in one line. 330 00:34:10,770 --> 00:34:14,070 What did we learn? Right? We learned that. 331 00:34:15,800 --> 00:34:21,440 For software verification. In software development, you can code without fear, right? 332 00:34:21,770 --> 00:34:26,180 You can implement optimisations that should before. 333 00:34:26,480 --> 00:34:34,850 Sometimes the person implementing or making the modification does not know all the assumptions that are needed for that to work. 334 00:34:35,750 --> 00:34:39,740 They know something, but they are not fully confident about the methods. 335 00:34:40,290 --> 00:34:43,880 You now have a proof of system to double check what you wrote. 336 00:34:45,050 --> 00:34:46,790 Both. Automation is essential. 337 00:34:47,120 --> 00:34:55,430 Link has been used in many different applications verified compilers, Polish languages, cryptography, cryptographic libraries, and so on. 338 00:34:55,640 --> 00:34:58,430 You can find all the projects in his effort. 339 00:34:58,820 --> 00:35:06,230 He's like a repository, like crates that are used for rust, where all the packages that are open source foiling are available there. 340 00:35:06,770 --> 00:35:12,830 You can browse them such then you know, for each version of reading each package is compatible with. 341 00:35:14,630 --> 00:35:21,200 And if you want to learn more how lean is using software? You can also read this blog post I wrote for Amazon. 342 00:35:21,530 --> 00:35:27,500 How lean is used for coding and encoding math both directions. 343 00:35:29,020 --> 00:35:34,030 I will be very brief here in the eye because Kevin will tell you much more. 344 00:35:34,600 --> 00:35:40,960 I would just, uh, tell you the obvious that large language models are amazing, but they hallucinate. 345 00:35:42,010 --> 00:35:45,390 It's great that for maths you can check. 346 00:35:45,400 --> 00:35:55,420 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. 347 00:35:55,690 --> 00:36:03,040 Imagine one day large language models start proving maths like the formalised theorem automatically. 348 00:36:04,290 --> 00:36:08,220 The proof. The formal proofs more than 200 pages long. 349 00:36:09,250 --> 00:36:12,480 Would you trust? I mean the likelihoods. 350 00:36:12,490 --> 00:36:16,420 A life language model made a mistake in 100 pages. It's really high. 351 00:36:16,840 --> 00:36:23,720 But we can check now, right? Machine checkable proofs are the antidote to hallucinations in the. 352 00:36:26,100 --> 00:36:31,980 Uh, yeah. But the other that we talked about how lean can help I. 353 00:36:32,310 --> 00:36:38,340 But I can also help lean. Right. That's several groups that are building. 354 00:36:38,340 --> 00:36:43,620 I should predict the next move in the game and even to complete the game. 355 00:36:44,400 --> 00:36:49,800 You say try to help me. They will try to synthesise a proof for the whole game for you. 356 00:36:51,240 --> 00:36:54,350 Mean, dojo is a popular package from Caltech. 357 00:36:54,710 --> 00:37:00,220 It's great because everything's open source. The model, the data sets, the code. 358 00:37:00,230 --> 00:37:04,360 Everything's open. Right? Uh. 359 00:37:04,360 --> 00:37:10,719 There are also projects by OpenAI and methi where they solved some Olympiad problems in 2000. 360 00:37:10,720 --> 00:37:14,050 2 in 2020. 2022 2023. 361 00:37:15,460 --> 00:37:19,870 But the big news there was alpha proof last year. 362 00:37:20,470 --> 00:37:27,209 Offer proof is in the AI built by DeepMind's. Being something that's many people in the community. 363 00:37:27,210 --> 00:37:33,540 Effort was impossible to build a system that can get a silver medal in the animal rights. 364 00:37:33,810 --> 00:37:37,500 It's weeks before they announce these results. 365 00:37:38,530 --> 00:37:41,710 People in the community are saying, oh, this is going to take years. You will never happen. 366 00:37:41,720 --> 00:37:48,340 It's impossible. But now DeepMind has alpha proof that you could do it. 367 00:37:48,610 --> 00:37:53,350 Do you mean proofs? Right? That's machine checkable, right? 368 00:37:53,890 --> 00:37:57,400 Gives you absolute assurance about the correctness of the results. 369 00:37:59,720 --> 00:38:04,460 Well, the lessons here, I think. I'm sure you have many more. 370 00:38:05,120 --> 00:38:11,569 But one big issue here is that machine checkable proofs allow us to build a AI that does not hallucinates, 371 00:38:11,570 --> 00:38:17,240 writes AI gets better and better at understanding explaining link codes. 372 00:38:17,840 --> 00:38:24,740 For example to install. When he learned something, he said that he has such pitchy on his sides. 373 00:38:25,160 --> 00:38:28,340 He was asking questions and he learned link. 374 00:38:29,120 --> 00:38:33,409 With the help of ChatGPT, you can give a big link file. 375 00:38:33,410 --> 00:38:38,000 It will explain you in natural language what the file does right. 376 00:38:38,000 --> 00:38:44,660 It will help you. Okay. If you ask about this, what this move does, it will give you a really good explanation. 377 00:38:46,440 --> 00:38:52,420 Now in the future, for sure, we are going to have AI systems that can prove hotter than gas. 378 00:38:53,750 --> 00:39:03,710 Before we wrap up, I want to emphasise that's one thing that we talked a lot about machine checkable proofs. 379 00:39:04,670 --> 00:39:11,660 But another ingredient that enables decentralised collaboration in learning is the fact that learning is extensible. 380 00:39:12,590 --> 00:39:15,920 It turns out that link is implemented in link itself. 381 00:39:16,550 --> 00:39:26,120 Is a programming language. You can make sure. All right, the mathematicians, the Mathlete community, all the time, they change things themselves. 382 00:39:26,390 --> 00:39:30,379 They add their own moves. They make modifications to the system. 383 00:39:30,380 --> 00:39:34,790 They adds the whole new syntax. That's great for for maths. 384 00:39:36,740 --> 00:39:42,379 And the main point is that even if you make a mistake in a move, it doesn't matter. 385 00:39:42,380 --> 00:39:49,220 The kernel will catch its it. Making the system extensible I think was really important. 386 00:39:49,550 --> 00:39:56,290 Before the fraud this non-profit's falling. It started in 2000 2023. 387 00:39:56,300 --> 00:40:04,280 Sorry, ten years after we started the project would impossible to get through 2023 if lean was not extensible. 388 00:40:04,460 --> 00:40:14,140 There was no team right building link. And he remember the Leia riff that she mentioned at the beginning? 389 00:40:14,190 --> 00:40:19,090 Actually, this is a move. This was implemented by the math community. 390 00:40:19,660 --> 00:40:23,760 Easing side of math. Liberty's move was not implemented. 391 00:40:24,460 --> 00:40:30,310 I did not implemented. This move was implemented by their linked users. 392 00:40:30,610 --> 00:40:37,340 It's inside of math flip bifida site and Grimes just moves were also implemented jingling. 393 00:40:37,360 --> 00:40:43,149 You can see the code for link. You can see the code and say, oh, this doesn't do exactly what I want. 394 00:40:43,150 --> 00:40:46,180 I want you to do more. You can modify its. 395 00:40:48,860 --> 00:40:57,470 I know the fees. That link got very popular in the I because it's very easy to shoot prospects inside of Lynn. 396 00:40:58,160 --> 00:41:03,560 You can access Memphis data. It's okay when you formalising Lynn. 397 00:41:04,280 --> 00:41:08,720 Math becomes data that can be processed. But how do you access this data? 398 00:41:09,500 --> 00:41:16,280 You don't need any new programming language. You can use lead self truth prospecting side of the data. 399 00:41:17,030 --> 00:41:22,520 You can you can write a link function that traverses your proof objects. 400 00:41:23,850 --> 00:41:29,790 The dependency graph was built this way. Kim Boyce on the same one of the quantum uh, 401 00:41:29,790 --> 00:41:39,210 I was your breaks example wrote a tool for extracting data in usage by open AI method to extract data from leaf for training. 402 00:41:40,110 --> 00:41:45,510 The same idea of Introspecting only objects can be used to build animations. 403 00:41:45,870 --> 00:41:52,830 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. 404 00:41:53,790 --> 00:42:03,840 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. 405 00:42:06,160 --> 00:42:12,490 The Leaf Frog is a non-profit that's started, uh, in 2023. 406 00:42:13,560 --> 00:42:21,750 Has 19 members. Now unto me being possible to run the lean projects without support of this foundation. 407 00:42:22,140 --> 00:42:29,940 The mission is to prove the scalability, usability, documentation, proof automation and reach self-sustainability in five years. 408 00:42:30,480 --> 00:42:38,430 Well, really grateful for the support from the Simmons Foundation, the Sloan Foundation, Research Working, and Alex Core. 409 00:42:39,270 --> 00:42:42,690 It would be impossible to do it without the support. 410 00:42:43,620 --> 00:42:49,140 There are too many users now asking too many things in that user. 411 00:42:49,320 --> 00:42:52,379 People that want to use me for teaching that's want. 412 00:42:52,380 --> 00:43:01,740 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, 413 00:43:01,740 --> 00:43:08,460 people that she wants more scalability, people that she wants cheese wants that without a team is impossible. 414 00:43:10,980 --> 00:43:15,470 These non profits also do not happen without conversions. 415 00:43:15,480 --> 00:43:23,250 Research conversions came up with a new concept called the Far rule Focus Research Organisation. 416 00:43:23,940 --> 00:43:36,150 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. 417 00:43:36,450 --> 00:43:39,150 There's no profitability path for the projects, 418 00:43:39,360 --> 00:43:49,140 the many projects like that and conversion to support this kind of projects in help raising money and running the nonprofits. 419 00:43:49,470 --> 00:43:57,390 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. 420 00:43:59,230 --> 00:44:04,740 Live show by the numbers. Uh. Before the live show, we would have a [INAUDIBLE]. 421 00:44:04,750 --> 00:44:11,290 It would take a long time for each release. Right now, since the fro started two years ago. 422 00:44:11,290 --> 00:44:21,250 Almost three years ago, we had 19 releases, more than 4000 requests with bugfixes, new features, performance improvements, and so on. 423 00:44:21,700 --> 00:44:26,020 All the roadmap, our roadmaps are all publicly available. 424 00:44:26,440 --> 00:44:33,910 Since then, link appears three times in the New York Times, Quantum Magazine, several times Scientific American, and so on. 425 00:44:36,120 --> 00:44:39,150 The growth of the project also accelerated. 426 00:44:39,480 --> 00:44:45,600 If you such, we can count easily the number of projects using lean on GitHub that more than 4000. 427 00:44:45,780 --> 00:44:49,830 And then you see we can see the acceleration after the we started. 428 00:44:51,100 --> 00:44:55,060 The number of downloads from the Visual Studio Code plugin. 429 00:44:55,420 --> 00:44:58,510 We have data in the Visual Studio, but. Codes. 430 00:44:58,600 --> 00:45:03,550 Marketplace provides data, but the data starts in 2024. 431 00:45:03,940 --> 00:45:11,380 You can see there were more than 40,000 installations, new installations, not updates since 2024. 432 00:45:13,040 --> 00:45:17,380 How can you contribute to the project? There are many different ways you can contribute. 433 00:45:17,390 --> 00:45:24,770 You can help using math Lib right, is that you can join the sleep channel where the community gathers. 434 00:45:25,670 --> 00:45:30,320 If you have questions about link, your question is going to be answered in minutes there. 435 00:45:31,400 --> 00:45:36,470 If you are interested in machine learning kernels, you can contribute to class projects. 436 00:45:36,890 --> 00:45:40,459 If you want to participate in a big formalisation project. 437 00:45:40,460 --> 00:45:47,000 Maths projects. You can contribute to the Families Theorem formalisation project that Kevin is running. 438 00:45:47,900 --> 00:45:53,350 You can create your own your projects rights and you'll be indexed automatically by his envoy. 439 00:45:53,360 --> 00:46:00,049 If you host it on on GitHub, you can use link without installing anything. 440 00:46:00,050 --> 00:46:05,040 You can go to Life bottling link.org/using link please. 441 00:46:05,180 --> 00:46:08,570 It's math lib everything in your browser. 442 00:46:09,200 --> 00:46:18,140 You can also support the nonprofits, not just by providing funding and partnerships, but also for creating for the projects. 443 00:46:18,380 --> 00:46:22,610 It's super helpful for us. Advocacy is really important. 444 00:46:24,750 --> 00:46:28,050 Uh. Uh, I'm very happy to be here today. 445 00:46:28,470 --> 00:46:33,180 The message I want to communicate is that learning is an efficient programming language and proof assistance. 446 00:46:33,720 --> 00:46:41,190 The Muslim community is changing how math is done. It's not just about proving, but going beyond your cognitive abilities. 447 00:46:41,310 --> 00:46:47,640 Right. In the future, we are going to have AI that's will be an assistant to you. 448 00:46:47,880 --> 00:46:56,430 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? 449 00:46:56,610 --> 00:47:04,450 Lee will track the details. Right? Centralised collaboration allowed large teams to work together. 450 00:47:05,200 --> 00:47:08,650 You don't need to take the result of someone on faith anymore. 451 00:47:09,370 --> 00:47:10,300 Thank you very much.