1000-plus theorems project

Stream: general

[Bolton Bailey]

I found this "1000+ theorems" project for tracking theorems from wikipedia in my notes. I vaguely recall this being posted in the Zulip, but can't find the reference now. Is this project still active and accepting PRs?

[Bolton Bailey]

@Katja Berčič @Floris van Doorn

[Floris van Doorn]

It has barely started. On the Lean side we want to set up a bit of infrastructure (similar to 100.yaml) before we want to add entries in mass. This is on @Pietro Monticone's to do list, but he's been very busy and helpful with more important things :-)

[Floris van Doorn]

Here was my message to him with the plan I had for the 1000plus project on the Lean side. I'm sure Pietro wouldn't mind if you want to set up a 1000plus.yaml file and a webpage on leanprover-community.github.io and then add entries.
Floris van Doorn said:

The basic possibility is to copy 100.yaml and the corresponding page on the leanprover-community webpage.
The entries of the yaml file would be indexed by the Q-number + suffix.

Freek prefers if that the links are directly to the result in the library. However, I still want that in Mathlib we keep track of the Lean-name, because otherwise it will break all the time. In that case, I want that the 1000-plus repo links to a page like this:
https://leanprover-community.github.io/1000plus.html#Q1067156X
and that will redirect to something like
https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Nat#doc
(or https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Nat#src )

Even with the last option, it might be nice to have a webpage which lists all entries

[Pietro Monticone]

Yes, for more info, see the following:

• Website
• Repository
• Talk at HIM
  

[Pietro Monticone]

Floris van Doorn said:

Here was my message to him with the plan I had for the 1000plus project on the Lean side. I'm sure Pietro wouldn't mind if you want to set up a 1000plus.yaml file and a webpage on leanprover-community.github.io and then add entries.
Floris van Doorn said:

The basic possibility is to copy 100.yaml and the corresponding page on the leanprover-community webpage.
The entries of the yaml file would be indexed by the Q-number + suffix.

Freek prefers if that the links are directly to the result in the library. However, I still want that in Mathlib we keep track of the Lean-name, because otherwise it will break all the time. In that case, I want that the 1000-plus repo links to a page like this:
https://leanprover-community.github.io/1000plus.html#Q1067156X
and that will redirect to something like
https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Nat#doc
(or https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Nat#src )

Even with the last option, it might be nice to have a webpage which lists all entries

Yes, I definitely don't mind.

[Joseph Myers]

Considering this in comparison to other sources of lists of theorems we've discussed: the Wikipedia list it's based on does seem to have a bias to results where "name of theorem" has a Wikipedia article - where the theorem itself is the natural unit for a Wikipedia article rather than having an article about an area of mathematics, or a particular solved or partly solved problem, or a mathematical object whose interest derives from the theorem about it, that discusses the theorem in a broader context (a theorem can still be significant like that without the theorem itself being the unit that has its own article (or indeed having a short name that would be convenient for naming an article about the theorem at all)). I'm not sure how that bias in the Wikipedia list might best be addressed (to get it to include significant theorems that don't have a convenient short name with its own Wikipedia article).

There's a separate bias in that list against theorems whose common name says "conjecture" (e.g. I don't see the Poincaré conjecture listed there), but that could presumably be addressed simply by adding such entries to the Wikipedia list under their common name, despite that name not using the word "theorem".

[Michael Rothgang]

In case Pietro is too busy: I can also help with setting this up - in a week or two.

[Pietro Monticone]

Yes, I am very busy unfortunately. Happy to collaborate on this in a few weeks. Thank you, Michael.

[Alex Meiburg]

Other examples of important theorems that have their own Wikipedia article, but no "theorem" in the name, and aren't in the "List of theorems":

https://en.wikipedia.org/wiki/Hamming_bound
https://en.wikipedia.org/wiki/Markov%27s_inequality
https://en.wikipedia.org/wiki/Minkowski%E2%80%93Steiner_formula
https://en.wikipedia.org/wiki/Scheff%C3%A9%27s_lemma

(these are supposed to be representative - there are many other "___'s inequality" or "____'s formula" that spring to mind).

"Kleene's Theorem" is a page on Wikipedia, but redirects to "Regular Language", where it is mentioned way down the article:
https://en.wikipedia.org/wiki/Kleene's_theorem

A lot of the 'missing' ones can be found in https://en.wikipedia.org/wiki/List_of_inequalities, but a lot can't.

[Alex Meiburg]

For some of the theorems already listed, I question whether would really count as formalized "mathematics", because they rely on a very large context of physics and what is or isn't physically sensible:
https://en.wikipedia.org/wiki/Carnot%27s_theorem_(thermodynamics)
https://en.wikipedia.org/wiki/Adiabatic_theorem
https://en.wikipedia.org/wiki/Buckingham_%CF%80_theorem

Some others are called the "___ theorem", but really refer to more a class of theorems that can be proved for different structures:
https://en.wikipedia.org/wiki/Arrival_theorem
https://en.wikipedia.org/wiki/Shannon%27s_source_coding_theorem
https://en.wikipedia.org/wiki/Universal_approximation_theorem

As in, these are all theorems where people talking about introducing a model in a paper, and then one should prove the X theorem for that model in order to motivate it. e.g. When introducing a NN architecture, people want to prove a universal approximation theorem. So, it doesn't make sense to talk about formalizing a proof of "the universal approximation theorem". One could talk about formalizing a proof of the universal approximation theorem for "multi-layer perceptrons with at least one hidden layer".

[Alex Meiburg]

Generally I think that going by https://en.wikipedia.org/wiki/Category:Mathematical_theorems and its recursive children might be a better baseline list of theorems. Wikipedia is generally more invested in accurate/complete Category tags over maintaining List's.

[Joseph Myers]

I think there are several relevant things to be done for 1000-plus (all the things I'm listing here are intended to be independent of particular ITPs - not about any Lean-specific infrastructure for showing on our site which theorems have been formalized in Lean).

[Joseph Myers]

(A) Get 1000-plus to a minimum viable state. This means (a) it's clear how people can PR information about theorems proved in a particular ITP and have the website update promptly (at present , there are two PRs open since August and an open issue since August about guidelines for PRs) and (b) it's also clear how people can PR improvements to the infrastructure and get those acted on (in particular, whatever code was initially used to create the data in the repository from Wikipedia needs to be checked in so that other people can make improvements to it).

[Joseph Myers]

(B) Improvements to 1000-plus infrastructure. It needs a way to update the list as Wikipedia data changes. Because any list on Wikipedia will probably include some irrelevant pages (e.g. the physics theorems discussed above), it needs a list of exclusions checked into git. Because some Wikipedia pages will discuss multiple theorems rather than it being clearly well-defined from Wikipedia exactly what mathematical result is meant by a page, it needs a way to add extra information in 1000-plus to uniquely identify exactly what theorems are meant (including listing multiple theorems from the same Wikipedia page).

[Joseph Myers]

I think one of the major weaknesses of the 100-theorems list is that it's not always clear what specific result is meant, and it would be undesirable for 1000-plus to replicate that. For example, does "The Isoperimetric Theorem" mean a 2-dimensional result or an n-dimensional result? (In that case, I think both versions should get separate entries in the benchmark list. Of course it would take a while to go through all the existing entries and disambiguate them. But certainly, when adding a new ITP entry for a theorem that has at least one such entry, it's worth checking if both ITPs chose the same version, and disambiguating into two or more entries if not.)

[Joseph Myers]

(C) Improvements to the input data on Wikipedia. There are several different ways one might try to get lists of theorems from Wikipedia.

(a) "List of theorems", as used at present by 1000-plus.
(b) "List of theorems" together with child lists such as List of mathematical identities, List of inequalities, List of theorems called fundamental and List of lemmas (because of the bias in "List of theorems" against things not called "theorem").
(c) Category:Mathematical theorems.
(d) Category:Theorems (there are a few theorems filed directly there, which ought to be moved to a more specific subcategory; subcategories other than Category:Mathematical theorems are probably not very relevant for this project, however).
(e) Pages whose title contains key words such as "theorem", "lemma", "identity", "inequality" or "formula".

Spot checks suggest that, while most theorems are probably both on "List of theorems" and a subcategory of "Category:Mathematical theorems", a significant number are missing from one or both of those places. So to make the data better for our purposes - and improve Wikipedia at the same time - it would be desirable to use all of (a) through (e) above to identify as many pages as possible with mathematical theorems (manually excluding pages that aren't in fact relevant, but including pages where only part of the content is a section about a theorem), and then add such pages to "List of theorems" if missing from there, as well as adding them to an appropriate subcategory of "Category:Mathematical theorems" if missing from there. I think that "Category:Mathematical theorems" is probably a better long-term source for 1000-plus, but before moving to it we do need to make sure we're not losing anything currently on "List of theorems" by doing so.

[Joseph Myers]

Of course, if you have a favourite theorem (maybe one you've formalized) that meets Wikipedia notability criteria, but isn't currently covered on Wikipedia, then adding a high-quality Wikipedia article for that theorem both improves Wikipedia and enables it to be included in the 1000-plus list. Since Wikipedia notability is about reliable third-party sources, checking places such as textbooks, review articles, award citations and popular coverage in places such as Quanta may also be a good way to find notable theorems before checking if they are already covered. (It's probably best not to do this for your own theorems, however, to avoid conflict of interest issues - leave it to someone else to write Wikipedia articles for notable theorems you proved yourself.)

[Kevin Buzzard]

Re: precise specification of the question. Freek once told me that he was intentionally vague about this because he didn't want to penalise any work by saying "well you've done something but technically you haven't done the right thing". But perhaps times have now changed.

[Joseph Myers]

My suggestion is definitely to err on the side of listing multiple variants of a theorem (since we're not restricted to a fixed number like 100), which avoids "technically haven't done the right thing" because both versions can always be listed in such cases.

[Alex Meiburg]

Just as another maybe 'hard' example: https://en.wikipedia.org/wiki/Sobolev_inequality is a very good candidate I would want on a list of theorems. But this single Wikipedia article has at least 8 different named theorems (+1 more, the log-sobolev inequality, that is described here but has its separate own Wiki article).

[Patrick Massot]

I have good news for you Alex: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.37

[Alex Meiburg]

That is lovely. :) And I'm happy to see it. But my point is more that Wikipedia articles do not correspond terribly well 1-to-1 to theorems.

[Alex Meiburg]

I'm not much of a functional analysis person, but I should give this a read.

[Michael Rothgang]

Just to avoid radio silence: I have to finish some other things first, but should have a prototype by the end of this week/next Monday. In the mean-tie, here are two preliminary clean-ups, best merged in order: #19503 and https://github.com/leanprover-community/leanprover-community.github.io/pull/556.

[Michael Rothgang]

The former PR has been merged, so the webpage PR is ready to go.

[Edward van de Meent]

wouldn't it make sense to only use , to separate authors, just like the standard is for the copyright headers?

[Edward van de Meent]

rather than interjecting and everytime?

[Alex Meiburg]

I thinnkk this convention might come from LaTeX, where (in the references) it is typical to give authors as ' and ' separated? And then the software formats this however you like, typically with commas.

[Michael Rothgang]

Right, the convention is the same as for author fields in .bib files.

[Michael Rothgang]

Currently, 100.yml uses both and and , (and does so inconsistently). After the PR, it uses and to separate multiple authors of the same formalisation, and uses , to separate authors of different formalisations.

[Michael Rothgang]

I don't really mind how we paint this bikeshed, but I'd like to be consistent with the formatting we choose. The above is one such way.

[Michael Rothgang]

(Context: for the 1000+ theorems project, I'd like to generate a yaml file similar to 100.yaml automatically, so need to settle on some convention. I'd like to be consistent with 100.yaml.)

[Edward van de Meent]

Michael Rothgang said:

I'd like to be consistent with the formatting we choose

this i completely agree with without question. It was more that i found the choice of separator odd as I wasn't aware of a standard which uses and as separator, but i did know that there is one which uses , .

[Mario Carneiro]

using comma separators is troublesome if an author is listed with last name first like Carneiro, Mario

[Michael Rothgang]

Adding to that: how do you determine the first and last name of an author from a full name? (Case in point: "Floris van Doorn", I know some admin somewhere got this wrong.) One way is to write "van Doorn, Floris" - this will confuse some heuristics. (Biber also offers "Floris {van Doorn}"; this is not the only way.)
Note that this detail isn't relevant here.

[Michael Rothgang]

A detail that perhaps is relevant: if listing authors as First Last, Second Name, and Third Author, naively splitting will also cause issues. That also happened in the file. In short: standardising on a mere "and" will (while somewhat artificial), at least maintain consistency.

[Edward van de Meent]

i see...

[Edward van de Meent]

indeed, there's a comma in "Meent, Edward van de"

[Thomas Zhu]

I think another benefit of a 1000+ theorem list is that a newcomer can easily see which theorems are already done/in progress and which are open for contribution. Currently, when someone proposes to do theorem XYZ, there is always a possibility that someone had done it (or partially done it) several years ago in a mathlib3 pull request and the theorem name is some obscure string, and some manual Zulip-mining is needed. (Or even worse, if the existing progress is not found and then people do duplicate work)

[Ruben Van de Velde]

I wonder what next steps could be. Maybe an attribute like the stacks one that takes a wikidata identifier?

[Michael Rothgang]

another benefit of a 1000+ theorem list

Or even better: some obscure branch, or a project outside of mathlib. I bet I would find some student projects out there interesting, though not mathlib-ready. :-)

[Michael Rothgang]

Ruben Van de Velde said:

I wonder what next steps could be. Maybe an attribute like the stacks one that takes a wikidata identifier?

Thanks for asking! I can think of the following next steps.

1. Add a new file 1000.yaml, hook it up to check-yaml (so declaration names are verified to exist)

2. Think about how this file will be updated. I can think of, for example,
   (a) (upstream-first) submit a PR to the 1000+ theorem github repo, get that merged, then automatically update the mathlib file
   (b) (downstream-first) change the mathlib file, merge that and create a PR mirroring the changes upstream. Periodically verify that the files don't diverge.
   (c) some kind of bi-directional sync
   (d) some variant of (b), but with the source of truth being a @[wikipedia] tag, and the yaml file being auto-generated from that. (That would be harder to make bi-directional, though. One could merely warn if some formalisation is mentioned upstream, but no such declaration is tagged.)

3. Implement a solution to (2).

4. Fill in all theorems which already have Lean or mathlib formalisations and rejoice at so many entries being already present :-).
5. All discussions about which theorems to additionally include in that list.

[Michael Rothgang]

I have a prototype for (1) and (2)a, can push tomorrow (bedtime over here). I haven't thought much about option 2(b). For simple cases, a solution shouldn't be hard --- and a script which complains in case there are "difficult" conflicts, but solves all the "easy" cases by itself is already useful.

[Michael Rothgang]

Thinking about question 2, which solution would be best

• (a) is easiest to implement (already done), but presumably could be cumbersome on the mathlib side. When adding a theorem, it's nice if I can also tick off the formalisation in 1000.yaml.
• (b) I worry about the upstream table becoming stale/out of date. It would be nice to avoid this somehow.
• (c) Would be nicest to use; I wonder about implementation complexity. Perhaps combining solutions to (a) and (b) with some "duct tape" will already go a long way. Such machinery certainly exists in other contexts (such as the WPT test-suite).

Opinions very welcome!

[Ruben Van de Velde]

I would lean towards (d) then (b). With (a) we couldn't have CI verify that all the declarations still exist, and (c) is too much work for a proof of concept for a project that might well not go anywhere. I prefer (d) because I think it's better to keep metadata about specific declarations as close as possible to the declarations themselves. It helps with discoverability, it handles renames with no additional work, and any feedback is immediate in the editor rather than only being reported after CI ran.

As long as we have a script that can extract the annotations from mathlib and update the 1000-theorems project, I'm not worried about it going terribly stale while someone still cares about it

[Yaël Dillies]

Can we also make it easy (=no peer review) to edit the list of formalisations, so that we can mention partial projects?

[Joseph Myers]

Note that whatever approach we use needs to handle the cases where a single Wikidata identifier corresponds to more than one theorem (at present, these are typically the cases where Wikipedia's "List of theorems" links to parts of a page that discuss different theorems, I think - in the 1000-plus git repository, there are files such as Q4724004A.md or Q1067156X.md for such cases).

If Wikidata / Wikipedia identifiers appear in individual source files, it would be desirable to have CI that makes sure those identifiers are valid (both at the time they are added, and from time to time after then in case something was deleted / renamed on Wikipedia).

[Michael Rothgang]

#19634 does step 1 of the above: it adds 1000.yaml and hooks it up to the check-yaml infrastructure. It's fairly large, but almost all of it is the autogenerated file.

[Michael Rothgang]

I'm not committing the generation script in that PR, curious readers can find it at branch#MR-1000-theorems-infra.

[Michael Rothgang]

https://github.com/leanprover-community/leanprover-community.github.io/pull/558 updates the webpage accordingly. Needs the mathlib PR to be merged first.

[Michael Rothgang]

The above branch now has a prototype of step 2(b). The yaml formatting comes out to be different; that's not a rabbit hole I'm willing to sink lots of time into.

[Michael Rothgang]

See also https://github.com/1000-plus/1000-plus.github.io/pull/6 and https://github.com/1000-plus/1000-plus.github.io/pull/7, which came about from this work.

[Yaël Dillies]

I've opened #20470 to add some more info to 1000.yaml

[Michael Rothgang]

Thanks a lot! Looking at the diff, I have one request about the date field: can you change the dates to the form YYYY-MM-DD, please? This is what the upstream file format expects...

[Yaël Dillies]

Ah... but sometimes there isn't one precise date where the project was finished

[Yaël Dillies]

What date should I pick in the following situations?

1. The decl comes from a single PR, merged in the same year as the copyright of the file it introduces (if such file exists)
2. The decl comes from a single PR, merged in a later year than the copyright of the file it introduces (if such file exists)
3. The decl comes from a separate repo
4. The decl comes from my memory because Bhavik hasn't yet been able to dig the code out of his laptop

[Patrick Massot]

Yes, it’s not realistic to expect such a precise date in many cases.

[Michael Rothgang]

https://github.com/1000-plus/1000-plus.github.io/pull/10 (by Floris) proposes relaxing the upstream requirement

[Michael Rothgang]

Current PRs improving the infrastructure around this:

• https://github.com/leanprover-community/leanprover-community.github.io/pull/563 refactors the webpage (after this, the comment field can be re-enabled),
• #20078 adds an automatic check for 100.yaml and 1000.yaml, which should catch errors that would make the webpage fail to build much earlier

[Michael Rothgang]

Both PRs above have landed, as well as a follow-up fix in 20614, and #20554 adding some more data to the yaml file.

There is one last task which can use help. I know almost nothing about how to do it, so help is very warmly welcome. Currently, the count on both 1000.html and 1000-missing.html on the webpage has a bug --- it only considers a theorem formalised if there is an author entry for it in the yaml file. It would be much better to allow either an author, decl or decls attribute.

The correct fix is to edit this resp. this line, to check the author and doc_decls fields.

[Bryan Gin-ge Chen]

Nice catch! I think I can fix this in short order... :fingers_crossed:

[Michael Rothgang]

Very nice! When you have a PR, feel free to ask for my review.

[Bryan Gin-ge Chen]

Done!

[Ruben Van de Velde]

I was gonna suggest we add the newly proved Liouville's theorem from #16797 to 1000.yaml, but it seems like it isn't one of the three Liouville's theorems in the list :sweat_smile:

[Michael Rothgang]

I had the same idea... Sounds like a "PR" to wikipedia is in order :grinning:

[Ruben Van de Velde]

Wikipedia needs a list of lists of theorems named after a person

[Joseph Myers]

As I previously mentioned in this discussion - #general > 1000-plus theorems project @ 💬 - there are several sources of theorems on Wikipedia and it would be useful to systematically (in some more or less repeatable scripted way) look for plausibly relevant theorems in any of (a) through (e) in my previous message, that aren't on the "List of theorems" currently used by this project, and add them there (and also make sure they are all in an appropriate subcategory of "Category:Mathematical theorems").

To affect this project we'll also need automation for updating the list in 1000-plus from Wikipedia, possibly based on whatever was used to create the list in the first place. And then automation for updating our own copy of the list when the upstream one in 1000-plus changes.

[Joseph Myers]

I'd also like to suggest a smaller project to make the list as it appears on our website nicer: sort the theorems (both on the list of ones we have, and on the list of ones we don't have) by something more meaningful than the internal Wikidata Q-number (which is good for sorting data files, as a stable identifier that shouldn't change, but not so good as anything visible to normal website users). Specifically, since the upstream 1000-plus project has a top-level two-digit MSC number for each theorem, the corresponding MSC descriptions might be a good choice for section headings on the page (and then sort alphabetically by theorem name inside each section, say).

[Michael Rothgang]

I have automation for updating the mathlib file when the 1000-plus files change. It might not be perfect yet, but should certainly help.
And I believe Freek Wiedijk has a script for re-generating the files upstream.

[Michael Rothgang]

Ongoing PRs are

• https://github.com/leanprover-community/leanprover-community.github.io/pull/577 and https://github.com/leanprover-community/mathlib4/pull/20637, allowing to tag statements of theorems as well
• https://github.com/leanprover-community/leanprover-community.github.io/pull/576 (improving the webpage, awaiting-author).

The first two are ready for review; it's easier to merge the webpage PR first.

[Fredrik Bakke]

Hi Lean people!

I was pointed here following a discussion on 1000+theorems, Wikipedia's list of theorems, and other large lists of theorems on the internet. I wrote this quick script for scraping theorems from the nLab, and figured it might be of value to you. Here's the output of that script: https://github.com/fredrik-bakke/theorem-scraper/blob/main/nlab_output.txt

Cheers

[Joseph Myers]

Since 1000-plus chose to work based on the Wikipedia List of theorems, such a scraped list is probably mainly of use for Wikipedia projects (identifying theorems to write Wikipedia articles for if they meet Wikipedia notability criteria, or to add such theorems to the List of theorems page if the articles already exist but aren't linked there), rather than directly for 1000-plus work.

[Ruben Van de Velde]

I've been thinking we should have a wikidata attribute like the stacks one, that way we're not so limited by this particular list

[Fredrik Bakke]

Apologies if this is off-topic for this channel. I've posted a contribution on the relevant Wikipedia talk page listing every Wikipedia page with an associated Wikidata identifier that is listed as an instance of a theorem, **but which is not on Wikipedia's list of theorems, 1132 pages in total (presumably with some inaccuracies). I don't personally have the capacity to comb through the list to double-check the entries and classify them by field, but if anyone here would like to pick up on that I'd be very glad!

[Joseph Myers]

That's more than I was expecting (I'd guessed maybe 10-20% more theorems would be found if the list was completed to cover all theorems with Wikipedia articles), but I hope people do go through the list (or divide it up to go through together, etc.) to make Wikipedia's list more thorough. (And if there's a notable theorem you like but that's covered as part of a Wikipedia article on a broader topic, rather than one specifically about the theorem, it might not be found by this process but adding it to the Wikipedia list would still be good to get it on the 1000-plus list eventually.)