convex polytopes

Stream: maths

[Johan Commelin]

@Joseph Myers you might have written about this before, but do you have specific targets in mind with your formalization of euclidean geometry etc...?
Is it: all IMO geometry in general?

Your recent stuff seems to cover a lot of prereqs for the classification of Platonic solids. Is that something that you had on your bucket list?

[Joseph Myers]

I'm exploring formalization via formalizing solutions to an (easier than IMO) paper with one problem in each of the olympiad areas of algebra, combinatorics, geometry and number theory. The non-geometry problems were done some time ago, the geometry one has taken a while given the need to build up Euclidean geometry from scratch (but that also means it provided experience in building up a theory from scratch, as opposed to proving something given the basic theory already present) - I'm currently eight sorrys away from completing that problem. (All eight sorrys in what I think are mathlib-appropriate results, I have a full formalization of everything I think is specific to that problem.)

[Joseph Myers]

I don't have a specific plan for after that. I think it would be nice to have "the whole IMO syllabus" formalized (there's no written syllabus, but e.g. the 171 definitions and results in chapter 2 of the IMO Compendium would be a reasonable approximation - although there must be a very long tail of lemmas that are needed but are too obvious to appear in such lists, especially for combinatorial geometry, and some entries in that list would end up as several separate formal results). The big gaps in mathlib's coverage of olympiad maths as measured by that list are geometry and graph theory (and I know a lot more graph theory than geometry, but graph theory is also an area where there seems to be a lot more active development underway for mathlib). Or I might try something that's not olympiad maths at all.

[Kevin Buzzard]

Joseph do you understand the nature of the proof of the Robertson-Seymour theorem?

[Johan Commelin]

Cool, thanks for the details!

[Johan Commelin]

What do you think of classifying the platonic solids?

[Kevin Buzzard]

Could we use representation theory for this?

[Kevin Buzzard]

Would our resolutely noncomputable principles come back to bite us?

[Joseph Myers]

For Platonic solids: I don't have any plans there, though I find that kind of combinatorial geometry and results about groups of isometries more interesting than a lot of synthetic geometry olympiad problems. It might make sense to add some definitions about abstract polytopes before trying to state and prove results about flag-transitive realizations thereof in Euclidean space (with or without convexity requirements).

[Joseph Myers]

Although my PhD was in graph minors I wasn't doing the sort of thing involved in Robertson-Seymour and don't know the details of that proof.

[Joseph Myers]

I don't expect noncomputability to cause problems classifying Platonic solids (it's pretty obvious there can only be finitely many cases by considering angles at a vertex, and if you want there are explicit expressions for the vertex coordinates though there are certainly nicer ways of showing e.g. that a regular dodecahedron actually exists). When you get into non-convex (Kepler-Poinsot) polyhedra it's not obvious, but still not too hard to show, that there can only be finitely many cases. (But the best approach for mathlib isn't necessarily the most elementary. I don't know what approaches there might be using representation theory.)

[Heather Macbeth]

Joseph Myers said:

(But the best approach for mathlib isn't necessarily the most elementary. I don't know what approaches there might be using representation theory.)

That would be my thought, too -- shouldn't one be classifying finite subgroups of $SO(3)$?

[Patrick Massot]

The classification of Platonic solid is really an important milestone in the history of math, it would be nice to have.

[Heather Macbeth]

But one could wait a little bit until group actions are defined, and then prove the "real" theorem (which connects to the ADE classification and other fancy math): if $G$ is a finite subgroup of $SO(3)$, and $(n_i)_{i\in\mathcal{I}}$ is the list of stabilizer sizes of its orbits in the canonical action on $S^2$, then
$\sum_{i\in\mathcal{I}}\left(1-\frac{1}{n_i}\right)=2\left(1-\frac{1}{|G|}\right)$,
and this forces a short list of possibilities.

[Heather Macbeth]

Constructing the icosahedron is a little painful (all those $\sqrt{5}$'s), so wouldn't it be nice to do it as a byproduct of the representations of $A_5$?

[Patrick Massot]

I think we have group actions, but maybe not a lot of theorems there.

[Joseph Myers]

Heather Macbeth said:

But one could wait a little bit until group actions are defined, and then prove the "real" theorem (which connects to the ADE classification and other fancy math): if $G$ is a finite subgroup of $SO(3)$, and $(n_i)_{i\in\mathcal{I}}$ is the list of stabilizer sizes of its orbits in the canonical action on $S^2$, then
$\sum_{i\in\mathcal{I}}\left(1-\frac{1}{n_i}\right)=2\left(1-\frac{1}{|G|}\right)$,
and this forces a short list of possibilities.

That expression reminds me of an expression you get in the classification of tile-transitive plane tilings ($\sum\left(1-\frac{2}{j_i}\right)=2$ where the $j_i$ are the degrees of the vertices around each tile, in any topologically tile-transitive tiling satisfying certain well-behavedness conditions); deduced there from Euler's theorem for plane maps. But while you can certainly consider tilings as a limiting case of polytopes, the results may not be closely enough related to deduce them both from any common more general theorem.

[Heather Macbeth]

Joseph Myers said:

But while you can certainly consider tilings as a limiting case of polytopes, the results may not be closely enough related to deduce them both from any common more general theorem.

Actually you can -- I wrote up some notes on this when I was teaching group theory :)

[Joseph Myers]

Nice! I hope we see things like that in mathlib at some point in the future. (What we have about group actions is extremely basic at present.)

[Joseph Myers]

Stating the classifications of normal tile-transitive or topologically tile-transitive plane tilings would I suppose then run into needing to pick a definition of tilings in mathlib levels of generality, since that's not an area where authors tend to go for giving maximally general definitions or for making their somewhat general definitions consistent with the somewhat general definitions chosen by other authors.

[Heather Macbeth]

This is tricky. I would prefer to classify discrete rank-2 subgroups of $\operatorname{Isom}^+(\mathbb{R}^2)$, but that definitely sweeps some difficulties under the rug.

[Joseph Myers]

As far as I know, what mathlib has right now on isometry groups is the instance : group (α ≃ᵢ α) (for [emetric_space α]) and nothing more, so anything at all about such groups would be a good start!

[Peter Nelson]

Kevin Buzzard said:

Joseph do you understand the nature of the proof of the Robertson-Seymour theorem?

I just came across this and am curious - why did you ask this? I know a moderate amount about this proof and am happy to discuss this.

[Kevin Buzzard]

I asked because I know Joseph and I thought that if he had some understanding of the proof then he would be able to say some intelligent things about how difficult it would be to get it into Lean.

[Kevin Buzzard]

I was just wondering what kind of a monumental challenge it was. For FLT we are so far away that we cannot even state most of the key intermediate results about modular forms and Galois representations in Lean yet.

[Kevin Buzzard]

In fact this fact is one of the things which guides where I put my efforts -- I am well aware that we still need a whole lot of definitions and I'm currently trying to add a whole bunch in commutative algebra so that people can start experimenting with them to see if they work Ok.