Building the Mathematical Library of the Future

Lean is the basis for my favorite puzzle game of the past five years: <a href="https:&#x2F;&#x2F;wwwf.imperial.ac.uk&#x2F;~buzzard&#x2F;xena&#x2F;natural_number_game&#x2F;" rel="nofollow">https:&#x2F;&#x2F;wwwf.imperial.ac.uk&#x2F;~buzzard&#x2F;xena&#x2F;natural_number_gam...</a><p>It&#x27;s like enemies &amp; bosses are mathematical theorems you have to prove. Each time you slay one, you get it as a weapon you can use against further, more difficult bosses! The grand finale (Inequality World) is very memorable; such a feeling of accomplishment after I cracked it all. Then you zoom out and realize the math you&#x27;ve defeated reaches, like, fourth grade at most.<p>Lean revolutionized my understanding of math itself, which I wrote about here: <a href="https:&#x2F;&#x2F;ahelwer.ca&#x2F;post&#x2F;2020-04-05-lean-assignment&#x2F;" rel="nofollow">https:&#x2F;&#x2F;ahelwer.ca&#x2F;post&#x2F;2020-04-05-lean-assignment&#x2F;</a>

I’ve long awaited the day we have automated proof checking. As someone who started in CS but went for a degree in Mathematics I held on to the idea of some sort of test suite that newer mathematicians (who have tend to come up with already existing or already disproven proofs for fun while thinking they’re on to something) could run to determine if they’re wasting their time and it not have to be a class mate making fun of them (sadly I’ve done this to kids who were just excited to try and learn, as if I had any room to talk.)<p>And it would only scale from there, hell we could run such a test suite against all known proofs and who knows how many ancient theorems we could disprove. I don’t think this is the test suite but something like it and the ANN that OpenAI build to check proofs is a good start.

There are several proof assistants trying to do what lean is doing (Coq, Isabelle to name but a few). Some of them have very well funded research projects with similar goals: <a href="https:&#x2F;&#x2F;cordis.europa.eu&#x2F;project&#x2F;id&#x2F;742178" rel="nofollow">https:&#x2F;&#x2F;cordis.europa.eu&#x2F;project&#x2F;id&#x2F;742178</a><p>When programming &#x27;business logic&#x27;, the multitude of programming languages is a good thing- it allows one to choose the best way to model a problem.<p>With computer aided proofs, I do wonder if the multitude of systems trying to create a mathematical library of Alexandria is a good thing.<p>Essentially they&#x27;re re-formalising the same theorems across different languages. Certainly some languages will model a specific problem better, but it does feel like a duplication of effort.

This is actually pretty cool. Every time theorem proving comes up, I make some mild complaints about not having any examples from real analysis or calculus like the mean value theorem. They in fact do and they can be found here [1]. Personally, I don&#x27;t find it particularly easy to read, but I am appreciative that there are some good examples of proofs that more people would be familiar with than, for example something from number theory.<p>[1] <a href="https:&#x2F;&#x2F;leanprover-community.github.io&#x2F;mathlib_docs&#x2F;analysis&#x2F;calculus&#x2F;mean_value.html" rel="nofollow">https:&#x2F;&#x2F;leanprover-community.github.io&#x2F;mathlib_docs&#x2F;analysis...</a>

Video demonstrating what it&#x27;s like to use Lean interactively:<p><a href="https:&#x2F;&#x2F;www.youtube.com&#x2F;watch?v=p4IrbnPomXg" rel="nofollow">https:&#x2F;&#x2F;www.youtube.com&#x2F;watch?v=p4IrbnPomXg</a>

Here’s a nice paper and talk by the mathlib folks at a January 2020 proofs and certified programs conf <a href="https:&#x2F;&#x2F;popl20.sigplan.org&#x2F;details&#x2F;CPP-2020-papers&#x2F;14&#x2F;The-Lean-mathematical-library" rel="nofollow">https:&#x2F;&#x2F;popl20.sigplan.org&#x2F;details&#x2F;CPP-2020-papers&#x2F;14&#x2F;The-Le...</a><p>Might be fun reading for folks

See also<p>The Mathematical Functions Grimoire <a href="http:&#x2F;&#x2F;fungrim.org&#x2F;" rel="nofollow">http:&#x2F;&#x2F;fungrim.org&#x2F;</a><p>The Future of Mathematics? [video] (youtube.com) <a href="https:&#x2F;&#x2F;news.ycombinator.com&#x2F;item?id=21200721" rel="nofollow">https:&#x2F;&#x2F;news.ycombinator.com&#x2F;item?id=21200721</a>

One cool thing about Lean is that the next version is trying to become something like a general-purpose programming language, with the idea of &quot;using proofs to write more efficient code.&quot;<p>For example, you might prove that your code never accesses a buffer out of bounds, so you can remove all your bounds checks for efficiency. Another example is implementing recursive functions with induction -- you can implement Fibonacci naively (fib 0 = 0, fib 1 = 1, fib n = (fib n-2) + (fib n-1)) and Lean will rewrite it into an efficient (non-exponential) form.<p>See: <a href="https:&#x2F;&#x2F;leanprover.github.io&#x2F;talks&#x2F;LeanPLDI.pdf" rel="nofollow">https:&#x2F;&#x2F;leanprover.github.io&#x2F;talks&#x2F;LeanPLDI.pdf</a>

I wonder if in addition to the proofs this could also be used to provide generated &quot;meta textbooks&quot;. The towers of theorems must be a graph, right? So shouldn&#x27;t I be able to say &quot;I want to understand Calabi–Yau manifolds&quot; and get a custom-made exercise set all the way down to set theory?<p>Add an invertible &quot;examples&quot; generator so examples can become exercises and keep track of all the exercises you&#x27;ve already done (perhaps with some kind of spaced-repetition system built in) and you can just keep &quot;fleshing out&quot; your own graph of practiced math knowledge starting with wherever you want to look next.

As I understand, Lean is a dependently typed programming language. How does it compare to a language like Idris?<p>How come mathematicians are encoding math in Lean instead of Idris for example?<p>Someone please correct me, I don&#x27;t know much about this at all, but I was under the impression that Lean is in a more &quot;imperative&quot; style, while Idris is a functional language. I would have guessed that a functional language would be a better fit for describing math.