Attributions for "100 theorems"

Question

Attributions for "100 theorems"

Closed this issue 25 days ago · 6 comments

fredrik-bakke commented a month ago

If we are to give credit to the original formalizers of the "100 theorems" theorems, we need to know who they are.

For easy reference, the agda-unimath page on "Formalizing 100 Theorems":

https://unimath.github.io/agda-unimath/literature.100-theorems.html

The List

Here's a~~n incomplete~~ list, please update it or comment with additional information.

3. The Denumerability of the Rational Numbers, Fredrik Bakke
11. The Infinitude of Primes, Egbert Rijke
25. Schröder–Bernstein Theorem, Elif Uskuplu
44. The Binomial Theorem, Egbert Rijke
60. Bezout's Lemma/Theorem, Brian Lu (blu-bird)
63. Cantor's Theorem, Egbert Rijke
69. Greatest Common Divisor Algorithm, Egbert Rijke
74. The Principle of Mathematical Induction, Egbert Rijke
80. The Fundamental Theorem of Arithmetic, Victor Blanchi
91. The Triangle Inequality, malarbol

Answer 1 · 2024-10-24T15:00:57.000Z

I added some names

Answer 2 · 2024-10-24T15:03:05.000Z

Thank you! I'll review the remaining ones when I find the time

Answer 3 · 2024-10-24T15:20:11.000Z

Perhaps it would also be good to explain a policy about what names are added, at the top of the file. For instance, we could mention that

the given names are of people who added the result to agda-unimath, even if the result is ported from another library.
If a result is ported from another library, then we try to be clear about it. For instance the CSBE theorem was ported from type-topology.
Sometimes significant improvements or alternative versions of theorems are added after the original contribution of a theorem. In this case we also try to mention those and attribute them accordingly. (eg this will be relevant for the constructive CSB theorem), and perhaps when someone simplifies the formalization of the Bezout theorem we could also add that.

Answer 4 · 2024-10-24T15:56:24.000Z

Bezout's lemma was added by blu-bird. He is currently not credited on either page on the Bezout lemma (for natural numbers, for integers), which is not great.

Answer 5 · 2024-10-24T16:20:57.000Z

Cantor's theorem was added by me, but is also not credited on the page. This is quite a big disadvantage of the automated crediting, given that it doesn't keep track when contents are moved to different files.

Answer 6 · 2024-10-24T19:45:37.000Z

Definitely not good!