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.
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.
