Participate in "1000+ theorems" project

[fredrik-bakke]

Properly participating in the 1000+ theorems has a couple of blockers on their side:

• Add support for the Agda proof assistant 1000-plus/1000-plus.github.io#22
• Clarify library classification 1000-plus/1000-plus.github.io#23
• Add stable hyperlinkable anchors to rows 1000-plus/1000-plus.github.io#24

This issue is a branch-out from #1214.

Formalized theorems

• Bezout's lemma, by Bryan Lu
• Binomial theorem, by Egbert Rijke
• Cantor–Schröder–Bernstein theorem, by Elif Uskuplu
• Cantor's theorem, by Egbert Rijke
• Cayley's theorem
• Diaconescu's theorem, by Fredrik Bakke Logic #1226
• Euclid's theorem, by Egbert Rijke
• Fundamental theorem of arithmetic, by Victor Blanchi
• Fundamental theorem of equivalence relations, by Egbert Rijke
• Kleene's fixed point theorem, by Fredrik Bakke
• Knaster–Tarski fixed point theorem, by Fredrik Bakke
• Lawvere's fixed point theorem
• Nicomachus's theorem, by Egbert Rijke Refactor elementary number theory #1211
• Yoneda lemma, by Emily Riehl

Useful links

• 1000-plus.github.io
• 1000-plus/1000-plus.github.io on GitHub
• List of theorems on Wikipedia

[VojtechStep]

I see that they have a script to sync with mathlib formalization. We could offer a similar script, since we already expose a machine-readable list of concepts, including wikidata IDs where possible, at https://unimath.github.io/agda-unimath/concept_index.json.

[fredrik-bakke]

That would be amazing!

[fredrik-bakke]

Note that I posted an issue there about Wikidata identifiers, as it turns out not every theorem on Wikipedia has a Wikidata identifier. There's also a standing issue about switching the identifier system on their side, although it seems the developers decided against it.

[fredrik-bakke]

@VojtechStep Do you see a way to link to a row in the 1000+ theorems table, either the index one or the all one? Am I stupid or do they not have a way to link to an entry??

[VojtechStep]

Nope, I don't see a way without adding upstream support (I was thinking of text fragments, but in this scenario they would be fragile and aren't supported by e.g. Brave)

[fredrik-bakke]

Alright, I'll write another issue to them

[fredrik-bakke]

Would it be enough to change <tr> to <tr id="{{ t.wikidata }}">? I don't know how that interplays with their page system

[fredrik-bakke]

I'll test locally

[VojtechStep]

I wouldn't expect the paging system to play nice with this out of the box, so I'd start by focusing on the All page. I also haven't looked if a wikidata identifier necessarily uniquely identifies a table row (for example it's not uncommon for agda-unimath to have multiple concepts tagged with the same wikidata id, it wouldn't surprise me if other systems had the same behavior).

[fredrik-bakke]

My understanding is that, by design, they're assuming Wikidata identifiers exist uniquely for every row c.f. issue 3 loc.cit.

[fredrik-bakke]

I went ahead and posted pull requests for all the upstream issues.