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