Martin Winter
@MWinter@mathstodon.xyz
There are *no* polytopes in mathlib!
The reason is not that no one is trying. People really like formalizing polytopes, and there are many independent proposals. We have our own of course: https://github.com/ooovi/Polyhedral. Took us a year to get here, no auto-formalization, but in return, mathlib quality.
Here is the real problem: mathlib in general, but its convex-geometry fragment in particular, is lacking reviewers. There are many open PRs in convexity, but too few people to check them. And nothing gets into mathlib without careful review.
If you can read Lean and you like convexity/polytopes, please help!