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.
- 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?
- 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?
- 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.