22
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ This question was motivated by the comments to this answer. In particular, I think others think what I'm proposing is unrealistic or unhelpful to the vast majority of the community and that is fine if it is the case. $\endgroup$
    – Jason Rute
    Feb 12, 2022 at 16:52
  • $\begingroup$ You're inviting opinions here. I'll give you one :-) $\endgroup$ Feb 12, 2022 at 16:55
  • $\begingroup$ Surely there are lots of "next things" given that many things are happening at once. I guess it makes sense to call something the successor of Freek's list if (1) the next thing is the most important thing happening to formal theorem proving, and Freek's list was previously the most important thing happening to formal theorem proving (this claim is doubtful) or (2) the next thing is the new most important list of theorems to work on (this shouldn't be too hard to achieve, given that Freek's list is almost done and there is no pre-existing competitor I'm aware of). $\endgroup$
    – Will Sawin
    Feb 12, 2022 at 22:37
  • $\begingroup$ @WillSawin. I was thinking closer to (2). Maybe I asked this question poorly. I didn't mean the "next thing" in the whole field as much as a replacement to Freek's list or something to fill a similar hole. For example, a few times Lean has talked about making their own list, and I thought it would be better to have it be discussed among the different communities. (However I've also been told that really almost all of the proof assistant community doesn't care about mathematics as much as software verification so such as list is not as much value to them.) $\endgroup$
    – Jason Rute
    Feb 12, 2022 at 22:46

3 Answers 3

16
$\begingroup$

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.

$\endgroup$
7
  • $\begingroup$ I think you and I have a different opinion on what the word "next" means. Or maybe we just have a different view on the operator associativity of and_then. $\endgroup$
    – Jason Rute
    Feb 12, 2022 at 16:59
  • 1
    $\begingroup$ You gotta shoot for the stars. Ok, I will modify my answer to something real. Hopefully the downvoters will change their minds :-) $\endgroup$ Feb 12, 2022 at 19:42
  • 1
    $\begingroup$ We just should outsource this to applied mathematics culture which is somehow resistant to inventors ambitions at least in area of pure math. $\endgroup$ Feb 12, 2022 at 23:44
  • 1
    $\begingroup$ @user9716869: Do you think we're making non-powerful proof assistants on purpose? $\endgroup$ Feb 13, 2022 at 17:23
  • 1
    $\begingroup$ It's a catch 22: if PAs are not adopted widely, there won't be enough pressure to improve them, but they are not adopted widely because they're not good enough. (I hope we can all agree that the current PAs are not good enough.) The plan "let's make a great PA first and convince people to use it later" is not going to work that well. $\endgroup$ Feb 13, 2022 at 22:52
16
$\begingroup$

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.

$\endgroup$
1
  • 2
    $\begingroup$ For 1, probably the Stacks project is the closest well-defined (but shifting...) thing to "What do researchers in a particular field (in this case, algebraic geometry) take for granted?" although it's not incredibly close, depending on which researcher in algebraic geometry you're talking about - perhaps it's pretty close to what Johan de Jong takes for granted, but I'm not even sure about that. $\endgroup$
    – Will Sawin
    Feb 13, 2022 at 13:00
11
$\begingroup$

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:

  1. 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.
$\endgroup$
2
  • 2
    $\begingroup$ I have a PhD student working on formalising GAGA in Lean, because Langlands-Tunnell produces a holomorphic function on the upper half plane but Wiles wants a global section of a sheaf on a scheme. This list is great. I have also been motivated by global class field theory; a post-doc of mine has recently formalised adeles and ideles, and a PhD student at Imperial has group cohomology. It would be interesting to formalise the statements of what Langlands needs from GCFT to state and prove local and global Langlands for abelian algebraic groups (the only paper of Langlands' I've ever read). $\endgroup$ Feb 13, 2022 at 22:41
  • 1
    $\begingroup$ @KevinBuzzard Thanks! I guess it's implicit in your comment that your preferred list of theorems bears a close relationship with the list of prerequisites of Wiles' and Taylor Wiles' papers on Fermat. (Could one make an actual numbered list of this, say by borrowing from the bibliographies of those papers?) For instance, to me that seems a somewhat strange reason to formalize GAGA... I guess for class field theory there is a steadily increasing series of more general / powerful theorems - it's not clear where to put the cutoff, other than at the very end. $\endgroup$
    – Will Sawin
    Feb 14, 2022 at 1:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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