## Stream: maths

### Topic: convex polytopes

#### Johan Commelin (Sep 02 2020 at 13:26):

@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 (Sep 02 2020 at 13:46):

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 (Sep 02 2020 at 13:54):

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 (Sep 02 2020 at 13:55):

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

#### Johan Commelin (Sep 02 2020 at 13:55):

Cool, thanks for the details!

#### Johan Commelin (Sep 02 2020 at 13:56):

What do you think of classifying the platonic solids?

#### Kevin Buzzard (Sep 02 2020 at 13:56):

Could we use representation theory for this?

#### Kevin Buzzard (Sep 02 2020 at 13:56):

Would our resolutely noncomputable principles come back to bite us?

#### Joseph Myers (Sep 02 2020 at 13:58):

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 (Sep 02 2020 at 14:01):

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 (Sep 02 2020 at 14:11):

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 (Sep 02 2020 at 15:19):

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 (Sep 02 2020 at 15:26):

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

#### Heather Macbeth (Sep 02 2020 at 15:33):

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 (Sep 02 2020 at 15:39):

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 (Sep 02 2020 at 15:58):

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

#### Joseph Myers (Sep 02 2020 at 19:52):

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 (Sep 02 2020 at 20:11):

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 (Sep 03 2020 at 00:46):

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 (Sep 03 2020 at 00:51):

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 (Sep 03 2020 at 01:01):

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 (Sep 03 2020 at 01:30):

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 (Sep 24 2020 at 18:43):

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 (Sep 24 2020 at 19:03):

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 (Sep 24 2020 at 19:05):

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 (Sep 24 2020 at 19:06):

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.

Last updated: May 11 2021 at 16:22 UTC