🏅 Top traders

Tried to look for PRs that mention theorems from the list of the 26 theorems that are not added yet:

Old PRs that should be adopted:

• https://github.com/leanprover-community/mathlib/pull/10632 - Ceva's theorem, requires changes

• https://github.com/leanprover-community/mathlib/pull/2819 - Minkowsky's theorem, I don't know what's up here, the PR seems kinda old and abandoned

Also:

• this PR says it should be useful for Descartes' rule of signs: https://github.com/leanprover-community/mathlib/pull/14949

• in https://github.com/leanprover-community/mathlib/pull/16615, @mlavrent mentions working on Brouwer fixed point theorem, but I don't know where his PR is

Market seems to have slept on this for a while

@BoltonBailey what's up with Brouwer's fixed point theorem?

Tempted to buy Yes shares and then submit a PR :-)

@JoachimBreitner Apparently Brouwer's fixed point theorem is done but not PRed. I think Hermite-Lindemann was being worked on too recently. I myself was working on Descartes' Rule of Signs through #14916, you are welcome to adopt that.