Building the Mathematical Library of the Future
quantamagazine.org
quantamagazine.org
It's like enemies & 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've defeated reaches, like, fourth grade at most.
Lean revolutionized my understanding of math itself, which I wrote about here: https://ahelwer.ca/post/2020-04-05-lean-assignment/
I've been approaching proofs from a different angle, going through the book "How to prove it" and making a complicated setup to use an old applet recommended in the book (ProofDesigner, which requires old versions of Firefox to even load the applet). While that part helps with formal symbols, it's very rigid and aging compared to this fantastic resource and language.
Got me to go back and re-watch Kevin Buzzard's talk at MS Research in re: Lean, "The Future of Mathematics?"
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.
A proof system could identify cases where you need hidden assumptions in order to make proofs. In this case, you would get a null result from the oracle, which would be valuable in itself.
The proof checker could detect such errors in a purportedly clean proof.
You've got a point, but in this case you are barking at the wrong tree. Aren't they talking about automated proof-checking?
I've definitely had the experience of "I think this is a valid proof. I haven't seen it presented anywhere else, and I'm not super familiar with the subject matter. It feels a little socially awkward to ask someone to check if it is right", and I started trying to express it in Lean.
However, I found it difficult to get the implicit type parameters to work right, so I had trouble even formulating the claim in Lean. (the claim was a claim in category theory, and the category theory library for Lean has lots of implicit argument stuff, and probably shouldn't have been the first thing I tried to use Lean for. Also the claim I was trying to show is probably very simple for category theory people.)
For the second, understanding why and actually proving something can be related but they're not equivalent. Of course, the intuitive ideas can lead to the right formal technicalities but it is not always the case.
There are two aspects of mathematical proofs-communication of ideas and formal verification. Confusing these distinction can be dangerous and this is why mathematicians led to the area of type theory and formal proofs.
Voedovsky, you can google him to find who he was, lost his faith in "human proof checking" after some error on his peer-reviewed and published result was accidentally discovered after years of nobody doubting its validity.
He dreamed of the world where people do and enjoy mathematics freely leaving the boring parts to computers like mathematicians in nowadays don't worry about how their writing will be published and communicated. What we do is write a proof and leave actual typesetting to the computer. It's called (La)TeX.
What you're saying is like claiming this program is correct because its logic is correct without ever knowing whether the code itself would get compiled or not. More extremely, there's no value for having more and more pseudocodes that we don't know they'll ever terminate or not.
When programming 'business logic', the multitude of programming languages is a good thing- it allows one to choose the best way to model a problem.
With computer aided proofs, I do wonder if the multitude of systems trying to create a mathematical library of Alexandria is a good thing.
Essentially they'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.
And one of the efforts I personally find most interesting is Metamath Zero, which attempts to be an interchange format among other things, with connections to HOL and Lean. See section 5 of: https://arxiv.org/abs/1910.10703
I think there are many provers which theoretically could be used for this effort, and am not convinced Lean is the absolute best, but I applaud the community for actually going ahead and doing it, instead of farting around with tools and hoping the library will magically happen (a valid critique of HoTT in my opinion).
I do hope the translation systems are actively used to consolidate, rather than built as an academic exercise.
There seems to be a large gap between vision ('our project will encapsulate all of mathematics in one place') and reality ('our project will just proliferate another standard')
[0]: https://leanprover-community.github.io/mathlib_stats.html
Also, the Flyspeck project has formalised the proof of a pretty recent theorem as well, mostly in HOL-Light and Isabelle.
http://www.cs.ru.nl/%7Efreek/100/
The top ones (sorted from most to least complete) are HOL Light, Isabelle, Metamath, Coq, Mizar, and Lean. Lean actually has the fewest proofs of those systems, though of course there are advantages to Lean as well.
I think some duplication is inevitable because there are fundamental disagreements on "what is important".
One problem with most of them as a "store of proof knowledge" is that most of these proof systems don't (normally) store the proof in terms of axioms, definitions, and previously-proven theorems. Instead, they store a program (as a sequence of tactic statements) that, if run, is intended to help the prover rediscover the proof... assuming that tactics never change (even though they do). As a result, older proofs in some of these systems can no longer be verified as being correct. This is one thing that attracts me to Metamath; Metamath stores literally every step, with all mathematical knowledge (including all axioms and definitions) in the database, so proofs stay proven. It also makes verification super-fast, e.g., 28K theorems can be verified in less than 1 second.
Others believe other traits are important, so they end up with different systems.
As far as translations between systems, I'm very interested in what happens with Metamath Zero. That work might, in the end, enable mutual translations between various systems. We'll see!
Note that Lean is not so high on that list, but also note that serious theorem proving in Lean is less than 5 years old, whereas the other systems are (several) decades old. There are at least two entries on the list that have only been formalized in Lean, and not in any other system. We are catching up pretty quickly.
It's clear that this list has an important status. But in my opinion, building a library of undergrad maths, which is what what TFA is mainly about, is a lot more important. We are tracking our progress over at https://leanprover-community.github.io/undergrad.html
I am not aware of such an organized effort in other systems. Without such a fleshed-out undergrad library, we'll never get to systematic formalization of (post)grad mathematics.
There is one key difference with the theorem provers- many of them share this lofty goal of building a library, akin to a 'library of Alexandria' (The article discusses this vision, and the research project I linked to at Cambridge is called 'Alexandria').
It's a grand vision - to formalise all mathematical knowledge in a library.
This vision doesn't exist in the world of regular software.
Nobody to my mind has claimed they're building a library of Alexandria. You could make the claim for npm, but I might shed a tear if you did that.
[1] https://leanprover-community.github.io/mathlib_docs/analysis...
Might be fun reading for folks
The Mathematical Functions Grimoire http://fungrim.org/
The Future of Mathematics? [video] (youtube.com) https://news.ycombinator.com/item?id=21200721
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.
Add an invertible "examples" generator so examples can become exercises and keep track of all the exercises you've already done (perhaps with some kind of spaced-repetition system built in) and you can just keep "fleshing out" your own graph of practiced math knowledge starting with wherever you want to look next.
That is, you want to get to Z? Well, you start at A. But you can get there by the sequence B, D, H, R, Z, or you can get there by B, C, F, H, R, Z, or by B, C, F, J, Q, S, U, Z. There is more than one route to proving many important theorems.
One important property to note is that a fair number of theorems exist where you can prove A with B or prove B with A, so the underlying directed graph is definitely very cyclic.
I'm not sure if this is equivalent or related, but I'm imagining an object which can contain, let's call them hypernodes. For example, in the case where A and B mutually imply each other, (A, B) is a hypernode, which internally contains a graph representing the relationship between A and B, but that relationship can be ignored in the main graph. I imagine this would become untenable with a slightly more complex network, though.
From the best AGI project out there: A hypergraph is much like a graph, except that the edges, now called “hyperedges” can contain more than two vertexes. That is, the hyperedge, rather than being an ordered pair of vertexes, is an ordered list of vertexes. The metagraph takes the hypergraph concept one step further: the hyperedge may also contain other hyperedges. https://github.com/opencog/atomspace/blob/master/opencog/she...
Well, specifically, a bipartite directed graph equipped with the specific partition, but if the graph is connected[1], which it should be in this case, then the partition is uniquely defined.
I guess such a graph would define another directed graph which has as vertices, the subsets of the "theorem" vertices, and a directed edge from any such subset to another which has 1 more "theorem" vertex, exactly when the "theorem" vertex has (in the original graph) an antecedent proof vertex such that all of the antecedent theorem vertices of that proof vertex are elements of the original subset of the theorem vertices.
so, if G = (V, E) is the original graph of theorems and proofs, and T \subset V is the set of theorems,
V' := \{ S \subset A \}
\forall S \in V', t \in T, (S, S \cup t) \in E' iff :
t \not\in S, and \exists p \in V s.t. (p,t) \in E, and \forall t' \in T s.t. (t',p) , it holds that t' \in S.
G' _will_ be a directed acyclic graph, because all of the edges strictly increase the size of the set. Then, finding "how can one learn all the prerequisite proofs in order to learn [result]" can be rephrased as "given the current vertex of G' (which is the set of theorems one already knows), what is a path which will get to any of the vertices of G' which have as an element the desired element [result] of G ?". The graph G' would be exponentially large in the size of T, so probably should not be represented explicitly in memory, but it seems like some shortest path algorithms should still help with this? There are many other properties of the graph G' which I imagine would be helpful in constructing a shortest path.
[1] in the sense that if you forgot the direction of the edges, the result is connected, not in the sense that every pair of vertices can be connected by a directed path in both directions
I've described it as bipartite directed graph in the past, but a key element of what I describe is that the two sets of nodes generally inherit their properties in different ways. For one set, you need something to happen "for all" predecessors; for the other, it needs to happen "for any" predecessor. It's this extra property I have no name for.
How come mathematicians are encoding math in Lean instead of Idris for example?
Someone please correct me, I don't know much about this at all, but I was under the impression that Lean is in a more "imperative" style, while Idris is a functional language. I would have guessed that a functional language would be a better fit for describing math.
Idris is geared more towards programming than theorem proving, with the difference basically being that with the latter one cares about more than the types ("I didn't formalize my spec completely") so the specific inhabitant matters. That makes tactics a bit dangerous.
Now there is also a school of thought the finds this reliance on metaprogramming (imperative of other) ugly and a site indication the languages and libraries are not good enough yet. I'm sympathetic, but currently the pro-tactic crowd seems to have the edge.
Lastly, "Lean" is kind of the epitome of "success at all costs" in more ways than tactics: implementation in C++ rather than a nice functional language for dogfooding, willing to sacrifice some intuitionist sacred cows not strictly needed for classical compatibility, etc.
To be fair, the main author of Lean has been cloistered for two years writing the next version, Lean 4, which is written in its own (pure functional) language. The siren song is strong :)