How up-to-date is the missing theorems list?

Stream: mathlib4

[Noble Mushtak (he/him)]

I'm looking at this missing theorems list: https://leanprover-community.github.io/1000-missing.html and right off the bat, I see "Arrow's impossibility theorem" on the list. However, from the list of Lean projects (https://leanprover-community.github.io/lean_projects.html), there is this project: https://github.com/asouther4/lean-social-choice which claims it has a proof of Arrow's Impossibility Theorem. Does this mean the list just needs to be updated? If so, where do people submit a PR to update this list?

Also, in general, can this list be trusted? For example, this list has Bayes' Theorem and Fermat's Little Theorem, both of which seem pretty doable with undergrad math knowledge. Can someone confirm that these two theorems are actually known to not be formalized? If they aren't, I'd like to start work on adding these to mathlib, but I only want to tackle it if there are no known formalizations of these theorems

[Rémy Degenne]

The 1000 theorem project and that list are both fairly new. Don't trust that list. Search the doc for the theorem first.

[Rémy Degenne]

Here is Bayes theorem: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/ConditionalProbability.html#ProbabilityTheory.cond_eq_inv_mul_cond_mul

[Ruben Van de Velde]

See https://github.com/leanprover-community/mathlib4/blob/master/docs/1000.yaml for the data that generates that file; cc @Michael Rothgang

[Michael Rothgang]

I have an in-progress PR filling in more data. Lots of further help is welcome. Can't link that easily (from phone).

[Ruben Van de Velde]

#20113

[Michael Rothgang]

Thanks for your help in that PR!

[Michael Rothgang]

branch#MR-1000-add-entries has some more entries (I had compared everything until line 1600 there.)