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?

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

8 Answers 8

Reset to default
23
$\begingroup$

The Lean community maintains several of such lists:

Improve this answer
$\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$
    – Calvin Khor
    Commented Feb 9, 2022 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.

Improve this answer
$\endgroup$
18
$\begingroup$

Mizar publishes them quarterly in their journal Formalized Mathematics.

Improve this answer
$\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$
    – Calvin Khor
    Commented Feb 9, 2022 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$
    – Slawomir K.
    Commented Feb 12, 2022 at 10:48
17
$\begingroup$

Metamath has such an extensive interlinked library.

A list of theorems in metamath is available here.

Improve this answer
$\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$
    – Calvin Khor
    Commented Feb 9, 2022 at 6:33
  • 1
    $\begingroup$ Sounds like a good idea $\endgroup$
    – Couchy
    Commented Feb 9, 2022 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.

Improve this answer
$\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.

Improve this answer
$\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
    Commented Feb 12, 2022 at 14:04
  • $\begingroup$ Thank you, Jarl. I've fixed those now. $\endgroup$
    – Greg
    Commented Feb 13, 2022 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.

Improve this answer
$\endgroup$
8
  • 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
    Commented Feb 11, 2022 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$
    – Patrick Massot
    Commented Feb 11, 2022 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
    Commented Feb 11, 2022 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$
    – Patrick Massot
    Commented Feb 12, 2022 at 13:35
  • 1
    $\begingroup$ @JasonRute I'm afraid I have to disagree with Patrick. You've done the best job I can find compiling the available figures. The criticisms above are apparent but hyperbolic and of limited value because of the lack of an alternative; you did the best that's publicly available after fixing a question of interest. $\endgroup$
    – Ronald J. Zallman
    Commented Nov 16, 2022 at 21:42
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)
Improve this answer
$\endgroup$

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