The connection was lost. Trying to connect again.

Martin Winter

@MWinter@mathstodon.xyz View on mathstodon.xyz

Mathematician at the Max-Planck Institute for Mathematics in the Sciences (Leipzig, Germany).

martinwintermath.github.io/

  • 2 posts
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: 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!

GitHub GitHub - ooovi/Polyhedral: Getting polyhedral geometry to lean. Getting polyhedral geometry to lean. Contribute to ooovi/Polyhedral development by creating an account on GitHub.

· Public · edited

Martin Winter @MWinter@mathstodon.xyz

Here is a truncated dodecahedron, deforming while keeping unit edge lengths. Can this be real? mathoverflow.net/a/513195/1088

· Public · edited