{{ message }}

Instantly share code, notes, and snippets.

# tangentstorm/Poly100.thy

Last active Aug 9, 2018
start on a proof of the polyhedron formula
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters

### tangentstorm commented Jul 24, 2018 • edited

so: I made a start on enumerating the platonic solids for the list of 100 theorems, but I need some help:
it assumes that I've already proven euler's relation (which is also on the list). I haven't, but ignore that for now. :)

my question is how to approach the three items marked '!HELP!' in the text... they just seem like they ought to be easy to simplify.

NOTE: the plain isar *.thy file is here: https://github.com/tangentstorm/tangentlabs/blob/master/isar/Poly100.thy

### dominique-unruh commented Jul 24, 2018

For the "m<=5" I would try the following:
Instead of proving "s<=5", I would prove

``````have "s<=5" if "1/s + 1/m > 1/2" for s m
``````

From that, you can then conclude both "s<=5" and "m<=5" directly.

(I haven't checked if it all works out.)

### tangentstorm commented Jul 24, 2018

@dominique-unruh thanks! I'll give that a try for the next version!

### tangentstorm commented Jul 25, 2018

@int-e showed me how to rewrite a huge chunk of the middle section, so the redundancy just went away... I think this is really starting to shape up into something nice. :)