List of notable theorems #1214
Comments
|
Very much agree! I don't think we should restrict ourselves to what Wikipedia lists as notable either, although I expect it can be* a hairy endeavour to arbit what is and isn't notable. |
|
If we want to use an external source for the list of theorems, however, I can mention again Freek's new project named 1000+ theorems (which bases itself on the same list from wikipedia). |
|
The reason why I don't find that list sufficient is that the criteria for being on Wikipedia's list don't perfectly align with our interests. To be on Wikipedia's list the theorem needs to have a wikipedia article, meaning the theorem needs to have enough historical precedence or that someone sees a need for it to be accessible to a larger audience in a wikiformat (and has enough resources and expertise to write it). |
These are all reasons for me why that list is much better than any criteria any individual could come up with.
I'd say that this is of critical importance! A list of notable theorems shouldn't be determined by any small group of individual's interests. |
|
I see, so you wouldn't want a list of "notable theorems... in univalent mathematics"? |
|
I was thinking about a list of theorems that are of general interest. Such a list shows to a general audience that our library has results that are widely recognized for their importance. In some of them the univalence axiom will be used to prove them, by the nature of our library. I'm also open to having a separate list of notable theorems of univalent mathematics, but perhaps we shouldn't create a list that is heavily biased by the univalent point of view and call it a "list of notable theorems" without further qualifications. As a side remark, I would love it even more if some theorems of univalent mathematics become so notable that they are picked up by a general audience, get published in the Annals and get wikipedia articles written about them. |
|
Okay, you have me persuaded. Do we want to include the lists on fundamental theorems, conjectures, and lemmas as well? |
|
Sure! Let's say that we create such a list if we have at least 10 items to put in it? (To not embarrass ourselves:)) |
|
Okay :) I had in mind to prove Diaconescu's theorem at some point, but I can't commit to writing something like that at the moment. Shall the issue main body be updated to maintain a list of how many results we have? (So we know when we have 10 results) |
|
Very nice! It was an old observation by Bas Spitters and mine that the suspension of a proposition It's Theorem 10.1.14 in the HoTT book |
|
I started adding a few theorems I could think of to the main body of the issue. |
|
The following is a long-list of things named after people or otherwise notable objects. The way I compiled this was to copy-paste the everything file, and delete all files that seemed unsuitable for a list of notable objects. I included things named after people (although I excluded cartesian products) and other custom named things. I still might have missed a few things, but I tried not to make a judgment yet on whether it should go in any final list at all. I might have missed things and I'd be very happy to take suggestions |
|
I had no idea that there was a fundamental theorem of equivalence relations btw, but we have it in the library:) |
|
haha yep 😄 |
I snuck in Diaconescu's theorem as part of #1226 :) |
|
I'm perhaps coming around in my opinion, and think that it might be best/easiest if we just list every notable theorem in the library, whether it is in the wikipedia list or otherwise notable. The long list I provided above could be a good initial setup. If a theorem is on wikipedia or some online encyclopedia, then we can provide links. Is that ok with you? I can go ahead and make that list. |
|
Could you try and explain how we should qualify a theorem as notable then? Your long list seems to me to be too inclusive for the page to be useful for the use case I envisioned. |
|
At the very minimum, we should not include pages that contain just statements of theorems, and not formalizations of them. Perhaps you can draft a list of results you want to include? |
|
I'm thinking to create a list of "Notable formalization entries". I'd propose that these include any kind of notable formalized object, such as a definition, lemma, theorem, or conjecture. Reasons to include an entry in the list include, but are perhaps not restricted to:
The purpose of such a list would be to give an overview of the highlights of the agda-unimath library, and give a sense to the contents of the library at a glance. This list should give a sense of how the library compares to other libraries, at least to people who are familiar with another library they have in mind. |
|
I am unsure about your idea and I'll have to think about it some more. One of my worries is that it will be hard to maintain. Regardless, I suppose it doesn't exclude also having a list of notable theorems as judged by Wikipedia authors, and that allows us to participate in the eventual 1000plus project. |
|
I'm coming around to your idea, so let's try to find a good implementation of it. In some sense, specially named concepts is what is judged by mathematical subcommunities to be important enough that a special name is warranted, and based on that it is a reasonable metric for notability. The list is naturally partitioned by namespace, so perhaps we should maintain a list for each namespace and then compile all of those into a big list. The individual sublists can be featured in the main namespace modules. I notice that some entries are missing from your list though, so we should go over it a second time before implementing. The missing entries I've noticed are
I think we should also try to be very clear about whether the formalized entry is a statement/definition or proof too. |
|
Awesome! I can create a joint PR in the coming days where I can make an initial version, and then we take it from there. Thanks for observing that some notable entries were missing. They definitely should be included! |
Freek's list is weird and arbitrary, and although it is widely used as a benchmark by libraries of formalized mathematics and therefore it is important to track it on our library.
However, it would make sense to me if we have a separate list of "Notable theorems", in which we list theorems in alphabetic order that have been formalized in our library. A reference list could be Wikipedia's list of notable theorems. There are plenty of notable theorems that are within reach for us, that would be nice to have, but which wouldn't be highlighted in the 100 Theorems list. A benefit of this approach is that what is regarded as important is not determined by one person at one moment in time, but is continuously maintained by the mathematical community and does not have an arbitrary cutoff at 100.
Any thoughts on this?
Formalized notable theorems
Two fixed point theorems #1227
Two fixed point theorems #1227
The text was updated successfully, but these errors were encountered: