27
$\begingroup$

I recall many years ago seeing a very large and well-interlinked (by computer) list of verified results starting from base assumptions and leading to all sorts of things that naive me did not expect computers to be able to handle e.g. measure theory. I don't recall what software was used, and certainly don't see any sort of link on e.g. https://leanprover.github.io/.

Where can I find these types of lists?

$\endgroup$
2
  • 6
    $\begingroup$ This should be a wiki question/answer as no answer will be comprehensive. $\endgroup$ Feb 9 at 6:53
  • 2
    $\begingroup$ @AndrejBauer I have just flagged for this (I presume that's how it works here too) $\endgroup$ Feb 9 at 7:26

8 Answers 8

22
$\begingroup$

The Lean community maintains several of such lists:

$\endgroup$
1
  • $\begingroup$ Thank you! The immediate takeaway for me is that I should have checked the community page. I suppose did not because I wanted to find information by 'lurking' rather than ask a newbie question. $\endgroup$ Feb 9 at 4:40
21
$\begingroup$

Freek Wiedijk maintains a list of 100 theorems, and pointers to formalizations in many different systems: https://www.cs.ru.nl/~freek/100/

The 100 theorems on the list were chosen a long time ago (and not by Freek). Some people think they are not a great selection of "100 important results in mathematics" but nevertheless, this list has become a sort of de facto benchmark for theorem provers and their libraries.

$\endgroup$
18
$\begingroup$

Mizar publishes them quarterly in their journal Formalized Mathematics.

$\endgroup$
2
  • $\begingroup$ +1, this certainly fits what I was looking for. Mizar itself sounds amazing and I'm surprised it can already be used for a journal. $\endgroup$ Feb 9 at 4:15
  • 1
    $\begingroup$ "already" is a bit misleading here. As of now Mizar has served as the basis for the Journal of Formalized Mathematics for more than 30 years. $\endgroup$ Feb 12 at 10:48
17
$\begingroup$

Metamath has such an extensive interlinked library.

A list of theorems in metamath is available here.

$\endgroup$
2
  • $\begingroup$ Ah, this is the list I stumbled upon many years before! For instance here is the Lebesgue integral. Although, in hindsight there are many other lists such as the other answers. In other SEs I would consider the tag [big-list] / flag to make comm wiki, any thoughts..? $\endgroup$ Feb 9 at 6:33
  • 1
    $\begingroup$ Sounds like a good idea $\endgroup$
    – Couchy
    Feb 9 at 7:01
17
$\begingroup$

Coq has an official Coq opam repository (see the accompanying Package Index or that of coq.io). These make it easy to search contributed formalization packages and install them. There is also a curated list of Coq frameworks, libraries and tools in the awesome-coq project.

For Isabelle/HOL there is the Archive of formal proofs which has hundreds of contributions. You may browse the index to get a feel for what is in there. And it is growing rapidly, too.

$\endgroup$
12
$\begingroup$

If you're interested in homotopy type theoretical foundations, I took a stab just today at comparing what's in the various HoTT math libraries.

It's a list of both theorems and "theories", since I was trying to understand the relative overall scope and overlap of the libraries. But it's not a particularly defensible collection of such theories, it's just a prototype.

The table links out to the repositories of the seven projects I was examining, but of special note is the Coq HoTT project which has a nice table of contents.

$\endgroup$
2
  • $\begingroup$ Cool, I wasn't aware of the nice ToC generated by Coq HoTT! In your survey, you missed that we do have Eilenberg-Mac Lane spaces in Coq HoTT. Also, the Hurewicz theorem is wip in Coq HoTT, not Cubical Agda. $\endgroup$
    – Jarl
    Feb 12 at 14:04
  • $\begingroup$ Thank you, Jarl. I've fixed those now. $\endgroup$
    – Greg
    Feb 13 at 14:45
11
$\begingroup$

Most of the main theorem provers have central libraries of formal mathematics. Here I've including their official statistics (accurate as of 2022-02-10) and more importantly a link to where you can find up-to-date statistics.

$\endgroup$
8
  • $\begingroup$ This older paper lists the HOL-Light main library as having 2,239 theorems and Flyspeck (which I'm not sure I'd consider a mathematical library in the same way as the others) as having 23,323 theorems. $\endgroup$
    – Jason Rute
    Feb 11 at 1:52
  • 3
    $\begingroup$ This is a nice list! It's worth noting for nonexperts that each of these libraries differ in (a) how they count declarations and (b) what topics they include. For example, the Lean stats do not count meta declarations or "auto-generated" declarations like equational lemmas, constructors of inductive types, etc. The AFP contains many developments of formalized software and PL-focused topics that would not be found in the MML. One should be very cautious trying to compare systems with these statistics. $\endgroup$
    – Rob Lewis
    Feb 11 at 2:31
  • 2
    $\begingroup$ I think that counting theorems is completely meaningless here. What would be more interesting would be to have a list of interesting theorems with indications of where they are formalized, a bit like Freek's list but a lot more balanced and with a lot more theorems. $\endgroup$ Feb 11 at 12:29
  • 1
    $\begingroup$ @PatrickMassot I won't way "completely meaningless", but I see your point. However someone needs to implement such as list, get buy-in from all the other theorem proving communities, and keep it up-to-date for all the major libraries. Right now most libraries only keep the above statistics and Freek's 100 theorem list. I know Lean discussed some version 2.0 of Freek's list at some point. I think that would be a GREAT question on this site: What would version 2.0 of the "Formalizing 100 Theorems" list look like?. Do you want to ask it? :) $\endgroup$
    – Jason Rute
    Feb 11 at 14:04
  • 1
    $\begingroup$ @JasonRute I think you spend too much time with Lean/mathlib people and have an extremely distorted view of the use of proof assistants. There are probably 1000 times more software verification than maths done in proof assistants. Also such a list would face the difficult question of what it means that a theorem is done. Does it count if you write a new library proving a theorem about real numbers using a definition of real numbers that is incompatible with all other libraries from your proof assistant? And what if it builds only with a ten years old version of Coq? $\endgroup$ Feb 12 at 13:35
10
$\begingroup$

From a similar question asked at cs.stackexchange.com.

Note: Only added info not already noted in existing answers.

enter image description here

  • TPTP (Thousands of Problems for Theorem Provers)
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.