Reminder: We'd love to see more Metamath 100 proofs

[David A. Wheeler]

This is my vaguely periodic reminder that I'd love to see more proofs
from the Metamath 100 list.

Currently there are 74 proofs proven by Metamath from this list of 100 proofs:
http://us.metamath.org/mm_100.html

That means there are a few to go; you can see the missing ones here:
http://us.metamath.org/mm_100.html#todo

These include:
47. The Central Limit Theorem
50. The Number of Platonic Solids
53. π is Transcendental
59. The Laws of Large Numbers
62. Fair Games Theorem
100. Descartes Rule of Signs

I'd love to see a few more!
It will require only 9 more to tie Isabelle (83).

--- David A. Wheeler

[Thomas Brendan Leahy]

Well, I finally got the Poincaré-Miranda theorem done as I promised a year ago, along with a very restricted version of Brouwer's fixed point theorem.  What's left is to show that convex compact sets with nonempty interior are homeomorphic and that those with empty interior are homeomorphic to compact convex sets of lower dimension (allowing for induction from the trivial base case of a point).

[David A. Wheeler]

On August 21, 2020 3:31:49 AM EDT, Thomas Brendan Leahy <tbrend...@gmail.com> wrote:
>Well, I finally got the Poincaré-Miranda theorem done as I promised a
>year
>ago, along with a very restricted version of Brouwer's fixed point
>theorem. What's left is to show that convex compact sets with nonempty
>interior are homeomorphic and that those with empty interior are
>homeomorphic to compact convex sets of lower dimension (allowing for
>induction from the trivial base case of a point).

Spectacular, and congratulations!


--- David A.Wheeler

[fl]

Pretty happy to see Brouwer's famous theorem even if its scope has beeen restricted to the unit cube.

-- 

FL

[Thierry Arnoux]

Congratulations Thomas!

This is very impressive again!
It sounds like the last step to the full Brouwer fixed point theorem is not so big, is it?