# Where can I find lists of theorems that have been verified?

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?

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

The Lean community maintains several of such lists:

• 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. Feb 9 at 4:40

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.

Mizar publishes them quarterly in their journal Formalized Mathematics.

• +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. Feb 9 at 4:15
• "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. Feb 12 at 10:48

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.

Metamath has such an extensive interlinked library.

A list of theorems in metamath is available here.

• 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..? Feb 9 at 6:33
• Sounds like a good idea
– Couchy
Feb 9 at 7:01

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.

• 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.
– Jarl
Feb 12 at 14:04
• Thank you, Jarl. I've fixed those now.
– Greg
Feb 13 at 14:45

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