List of notable theorems

[EgbertRijke]

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

• The Fundamental Theorem of Arithmetic, by Victor Blanchi
• Fundamental theorem of equivalence relations
• The Binomial Theorem, by Egbert Rijke
• Cantor–Schröder–Bernstein theorem, by Elif Uskuplu
• Cantor's Theorem, by Egbert Rijke
• Cayley's Theorem
• Kleene's fixed point theorem, by Fredrik Bakke
  Two fixed point theorems #1227
• Knaster–Tarski fixed point theorem, by Fredrik Bakke
  Two fixed point theorems #1227
• Lawvere's fixed point theorem
• Bezout's lemma, by Bryan Lu
• Yoneda lemma, by Emily Riehl
• Diaconescu's theorem, by Fredrik Bakke Logic #1226

[fredrik-bakke]

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.

[fredrik-bakke]

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

https://1000-plus.github.io/

[fredrik-bakke]

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

[EgbertRijke]

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.

don't perfectly align with our interest.

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.

[fredrik-bakke]

I see, so you wouldn't want a list of "notable theorems... in univalent mathematics"?

[EgbertRijke]

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.

[fredrik-bakke]

Okay, you have me persuaded. Do we want to include the lists on fundamental theorems, conjectures, and lemmas as well?

[EgbertRijke]

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:))

[fredrik-bakke]

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)

[EgbertRijke]

Very nice! It was an old observation by Bas Spitters and mine that the suspension of a proposition P is equal to the set quotient 2/~ where 0~1 iff P, and we used this to derive Diaconescu's theorem at the time.

It's Theorem 10.1.14 in the HoTT book

[fredrik-bakke]

I started adding a few theorems I could think of to the main body of the issue.

[EgbertRijke]

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

category-theory.right-kan-extensions-precategories
category-theory.yoneda-lemma-categories
category-theory.yoneda-lemma-precategories
commutative-algebra.binomial-theorem-commutative-rings
commutative-algebra.binomial-theorem-commutative-semirings
commutative-algebra.eisenstein-integers
commutative-algebra.gaussian-integers
commutative-algebra.zariski-locale
commutative-algebra.zariski-topology
elementary-number-theory.ackermann-function
elementary-number-theory.bezouts-lemma-integers
elementary-number-theory.bezouts-lemma-natural-numbers
elementary-number-theory.binomial-theorem-integers
elementary-number-theory.binomial-theorem-natural-numbers
elementary-number-theory.catalan-numbers
elementary-number-theory.cofibonacci
elementary-number-theory.collatz-bijection
elementary-number-theory.collatz-conjecture
elementary-number-theory.dirichlet-convolution
elementary-number-theory.euclid-mullin-sequence
elementary-number-theory.euclidean-division-natural-numbers
elementary-number-theory.eulers-totient-function
elementary-number-theory.fermat-numbers
elementary-number-theory.fibonacci-sequence
elementary-number-theory.fundamental-theorem-of-arithmetic
elementary-number-theory.goldbach-conjecture
elementary-number-theory.hardy-ramanujan-number
elementary-number-theory.infinitude-of-primes
elementary-number-theory.jacobi-symbol
elementary-number-theory.kolakoski-sequence
elementary-number-theory.legendre-symbol
elementary-number-theory.mersenne-primes
elementary-number-theory.peano-arithmetic
elementary-number-theory.pisano-periods
elementary-number-theory.pythagorean-triples
elementary-number-theory.sieve-of-eratosthenes
elementary-number-theory.stirling-numbers-of-the-second-kind
elementary-number-theory.sylvesters-sequence
elementary-number-theory.taxicab-numbers
elementary-number-theory.telephone-numbers
elementary-number-theory.triangular-numbers
elementary-number-theory.twin-prime-conjecture
elementary-number-theory.well-ordering-principle-natural-numbers
elementary-number-theory.well-ordering-principle-standard-finite-types
finite-group-theory.abstract-quaternion-group
finite-group-theory.cartier-delooping-sign-homomorphism
finite-group-theory.concrete-quaternion-group
finite-group-theory.simpson-delooping-sign-homomorphism
foundation-core.univalence
foundation.axiom-of-choice
foundation.cantor-schroder-bernstein-escardo
foundation.cantors-theorem
foundation.descent-coproduct-types
foundation.descent-dependent-pair-types
foundation.descent-empty-types
foundation.descent-equivalences
foundation.dubuc-penon-compact-types
foundation.fundamental-theorem-of-identity-types
foundation.global-choice
foundation.hilberts-epsilon-operators
foundation.law-of-excluded-middle
foundation.lawveres-fixed-point-theorem
foundation.lesser-limited-principle-of-omniscience
foundation.limited-principle-of-omniscience
foundation.preunivalence
foundation.principle-of-omniscience
foundation.regensburg-extension-fundamental-theorem-of-identity-types
foundation.type-duality
foundation.type-theoretic-principle-of-choice
foundation.univalence-implies-function-extensionality
foundation.univalence
foundation.weak-function-extensionality
foundation.weak-limited-principle-of-omniscience
graph-theory.eulerian-circuits-undirected-graphs
graph-theory.stereoisomerism-enriched-undirected-graphs
group-theory.abelianization-groups
group-theory.cayleys-theorem
group-theory.dihedral-groups
group-theory.furstenberg-groups
higher-group-theory.eilenberg-mac-lane-spaces
lists.quicksort-lists
metric-spaces.cauchy-approximations-metric-spaces
metric-spaces.cauchy-approximations-premetric-spaces
order-theory.galois-connections-large-posets
order-theory.galois-connections
order-theory.zorns-lemma
real-numbers.dedekind-real-numbers
set-theory.baire-space
set-theory.cantor-space
set-theory.cantors-diagonal-argument
set-theory.russells-paradox
species.cauchy-composition-species-of-types-in-subuniverses
species.cauchy-composition-species-of-types
species.cauchy-exponentials-species-of-types-in-subuniverses
species.cauchy-exponentials-species-of-types
species.cauchy-products-species-of-types-in-subuniverses
species.cauchy-products-species-of-types
species.cauchy-series-species-of-types-in-subuniverses
species.cauchy-series-species-of-types
species.dirichlet-exponentials-species-of-types-in-subuniverses
species.dirichlet-exponentials-species-of-types
species.dirichlet-products-species-of-types-in-subuniverses
species.dirichlet-products-species-of-types
species.dirichlet-series-species-of-finite-inhabited-types
species.dirichlet-series-species-of-types-in-subuniverses
species.dirichlet-series-species-of-types
species.hasse-weil-species
species.products-cauchy-series-species-of-types-in-subuniverses
species.products-cauchy-series-species-of-types
species.products-dirichlet-series-species-of-finite-inhabited-types
species.products-dirichlet-series-species-of-types-in-subuniverses
species.products-dirichlet-series-species-of-types
species.small-cauchy-composition-species-of-finite-inhabited-types
species.small-cauchy-composition-species-of-types-in-subuniverses
species.unit-cauchy-composition-species-of-types-in-subuniverses
species.unit-cauchy-composition-species-of-types
species.unlabeled-structures-species
synthetic-homotopy-theory.cavallos-trick
synthetic-homotopy-theory.descent-circle
synthetic-homotopy-theory.descent-property-pushouts
synthetic-homotopy-theory.descent-property-sequential-colimits
synthetic-homotopy-theory.eckmann-hilton-argument
synthetic-homotopy-theory.flattening-lemma-coequalizers
synthetic-homotopy-theory.flattening-lemma-pushouts
synthetic-homotopy-theory.flattening-lemma-sequential-colimits
synthetic-homotopy-theory.hatchers-acyclic-type
synthetic-homotopy-theory.plus-principle
synthetic-homotopy-theory.universal-cover-circle
univalent-combinatorics.binomial-types
univalent-combinatorics.dedekind-finite-sets
univalent-combinatorics.ferrers-diagrams
univalent-combinatorics.kuratowski-finite-sets
univalent-combinatorics.latin-squares
univalent-combinatorics.main-classes-of-latin-hypercubes
univalent-combinatorics.main-classes-of-latin-squares
univalent-combinatorics.petri-nets
univalent-combinatorics.pi-finite-types
univalent-combinatorics.pigeonhole-principle
univalent-combinatorics.ramsey-theory
univalent-combinatorics.steiner-systems
univalent-combinatorics.steiner-triple-systems

[EgbertRijke]

I had no idea that there was a fundamental theorem of equivalence relations btw, but we have it in the library:)

[fredrik-bakke]

haha yep 😄

[fredrik-bakke]

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.

I snuck in Diaconescu's theorem as part of #1226 :)