[yaseer]

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: https://cordis.europa.eu/project/id/742178

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.

[raphlinus]

There is work on making proofs portable from one system to another. One effort is Dedukti, which is based on the idea that "lambda pi modulo" is a universal logic for theorem provers. A less ambitious effort is OpenTheory, which from what I can tell is mostly about being able to interoperate between different HOL flavors.

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

[dddbbb]

The author of the Metamath Zero paper is actually one of the most active contributors to the project described in the article[0].

[0]: https://leanprover-community.github.io/mathlib_stats.html

[yaseer]

Thanks for sharing! I Remember seeing Dedukti a while back, but I haven't seen some of these newer translation efforts.

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')

https://xkcd.com/927/

[dddbbb]

It seems to me like Lean has a lot of the momentum at the moment. It's clear that other projects like Coq suffer from a lack of traditional mathematicians formalising modern, fashionable topics. Kevin Buzzard's implementation in Lean of perfectoid spaces is a great example of that boundary being broken, as far as I can tell the most advanced Coq proofs are the four colour theorem and Feit-Thompson theorem, which have analogue proofs from the 60s and 70s.

[auggierose]

But you have to take into account that the Coq proofs are actual proofs of big THEOREMS. What Buzzard has done is implementing a big DEFINITION :-)

Also, the Flyspeck project has formalised the proof of a pretty recent theorem as well, mostly in HOL-Light and Isabelle.

[dwheeler]

There are indeed several different proof systems. "Formalizing 100 Theorems" tracks the progress of the "top" ones compared to a set of well-known proofs:

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!

[leanuser83]

(Disclaimer: I'm addicted to Lean. My view is biased.)

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.

[delusional]

The exact same thing is said about other programming languages.

[yaseer]

I agree, and discussed this a little.

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.