Impact of "Formalizing 100 Theorems" and what is next

Question

In the early 2000s (or maybe even earlier) Freek Wiedijk published a list of 100 theorems which were a sort of litmus test of the state of the art in formalized mathematics. As the completion rate nears a stable point, I want to ask the community's reflection on the list and its future.

1. Has Freek's list been a positive impetus to the community? Especially for the (much?) smaller half of the community focusing on developing libraries of formal mathematics?
2. As this list is nearly complete (save for FLT), what next? Do we need a new list, or something similar, to bring visibility to formal theorem proving, encourage growth, compare tools, and measure progress in the field?
3. If so, what would that next thing look like? Would it be just mathematics? Mathematics and software? Is there any hope that one could get buy-in from lots of proof assistant communities, or are their respective aims just too different? Who would maintain it? Or should each community just maintain their own lists according to their own standards?

Edit: I am mostly just asking if we need a new list or something similar to replace it, not asking what the next big thing in all of formal theorem proving needs to be. The immediate motivation for this question was a discussion about if there is any meaningful way to compare the various libraries of formal mathematics since they have different methods of counting theorems and some focus more on pure mathematics than others. While any individual or any proof assistant community can make their own list, I wanted to use this forum involving many different proof assistants to discuss if there is any agreement on this matter. I wrote the question a bit more broadly since I thought this list was a good way to measure progress in the field and show what can be done.

Answer 1

Freek's list served a very helpful purpose. It's nice to have a list of standard challenges which are recognisable to those outside the community, and its near-completion makes it very clear that it is possible to formally prove interesting theorems.

That said, we do not need another list. The point -- that it is possible to do serious mathematics in proof assistants -- has been made, and there's no sense in making the same point over and over again.

Now that we know it is possible, the next problem is showing that mechanised mathematics is convenient. Plenty of working mathematicians use tools like SageMath and Mathematica, and they do so because they makes computations, plotting, and algebraic manipulations much faster and more reliable. But very few people use Coq because it makes proofs easier[1]. For sensible mathematics, it is only a mild exaggeration to say proof assistants are actually proof obstructants!

In my view, there are two major intertwined problems.

1. We simply do not know how to build large and usable libraries of mechanised mathematics. A working mathematician has a large body of knowledge and standard facts at her fingertips, and can use them straightforwardly in her work. This is partly a matter of lacking experience, and partly a matter of not knowing which features are missing from our proof assistants.

   For example, the work in Coq on HierarchyBuilder is a good example of adding features to a proof assistant to support the needs of large-scale verification. Conversely,the Lean mathlib project is a very important attempt to work out how to design a large corpus ("the undergrad curriculum") by actually doing it.

2. No proof assistant has anything approaching a predictable envelope of operation.

   Complex tools need to have a clear and teachable set of principles of operation. Without a good mental model, it's very hard for a human operator to figure out which things they try will work, how things can go wrong, and how to repair errors when they do occur.

   At the moment, there are basically no proof assistants which satisfy this criterion. You basically have to understand the exact internals of the implementation to handle complex problems. And while one might be tempted to think this is impossible for decidability/complexity reasons, I think this is wrong.

   For example, SMT solvers actually do satisfy this criterion. If you stick to using quantifier-free combinations of decidable theories, they basically just work, even though the problems are NP-complete in general.

[1] It really does make your life easier when doing formal verification. If you need to revise the induction hypothesis on a seven-bajillion case induction over all the instructions, addressing modes, and protection levels of the ARM instruction set or something, then a proof assistant will save your life.

Answer 2

The next big thing is to achieve wide adoption of formalized mathematics among mathematicians.

This is a much harder problem than formalization of this or that theorem. It will be accomplished by a change of generation. The best we can do is to encourage our students to learn formalization at an early age, and to push for the recognition of formalization as honest mathematical work. It is ridiculous that the only thing that counts in one's scientific career is mathematical discovery.

Answer 3

Let me suggest three possible answers to the question "What should be the next list of math theorems to prove?" without any claim that such a list should be the most important thing in formal theorem proving generally, or even specifically in formalized mathematics.

1. One could simply follow the Lean/mathlib community and list the topics for an undergraduate degree in mathematics. Of course the expectations here vary between nations, institutions, and even within an institution. I guess if one wanted to formally track progress between formal theorem provers, it might make sense to start from the requirements of whichever famous university has the most well-defined curriculum.

2. If one wants a list of famous theorems which are of greater interest in modern mathematics than most of the Freek list, one could look at "Fields-medal winning theorems", i.e. the result of each Fields medal winner that was most famous and contributed most to their award, when that result exists and is relatively clear. This would be subjective, and one would have to make some arbitrary decisions, but a rough start would be:

• Kodaira embedding theorem

• Finiteness of homotopy groups of spheres or GAGA theorem (or both)

• Roth's theorem (not the arithmetic progressions one)

• $S^7$ has multiple non-diffeomorphic smooth structures

• Atiyah-Singer index theorem

• Independence of the continuum hypothesis from ZFC (already formalized) and maybe also Independence of the axiom of choice from ZF

• Generalized Poincaré conjecture in dimension $\geq 5$ (or maybe the h-cobordism theorem although I think the difficulty of proving them is very similar)

• Baker's theorem

• Resolution of singularities of algebraic varieties

• Pontryagin classes of a smooth compact manifold are invariant under homeomorphism

• Odd order theorem (already formalized) or maybe classification of minimal finite simple groups

• the Riemann hypothesis of the Weil conjectures

• Donaldson's theorem

• Faltings' theorem

• Generalized Poincaré conjecture in dimension $4$

• Restricted Burnside problem

• Langlands conjectures for the general linear group over function fields

• Milnor conjecture

• Poincaré conjecture or Geometrization conjecture

• Fundamental lemma

• Landau damping

• The average rank of elliptic curves is less than $1$

• Boundedness of Fano varieties

3. For an approach which is objective in the sense of not forcing the list-maker to make a lot of decisions on the details, but not at all objective in the sense of balance between different fields of mathematics, or in the sense of depending on much more than the thoughts of one person, one could count the number of tags in the Stacks project formalized in each proof assistant. This would count definitions as well as theorems. Keeping track of progress would be nontrivial as there are so many tags, but making new progress would pretty much always be in reach.