*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] New in the AFP: Formal Puiseux Series*From*: Mohammad Abdulaziz <mohammad.abdulaziz8 at gmail.com>*Date*: Fri, 26 Feb 2021 17:06:11 +0100*In-reply-to*: <f08adbc3-e10e-ec70-a1bc-39f205f8be1c@in.tum.de>*References*: <1DE7FA07-8F6E-444A-9420-F1F4878FA81C@cam.ac.uk> <0f8fbfdb-7d5a-c993-3ffc-4634134ee933@in.tum.de> <45F1642C-6AC5-4616-BBED-ED06C076920C@cam.ac.uk> <20210224163900.soz2nd2babfbn4kl@xb27-stretch.fritz.box> <f08adbc3-e10e-ec70-a1bc-39f205f8be1c@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.10.0

However, would this be enough to claim one has shown the Isoperimetric Theorem? To me, that sounds dangerously like making the theorem true by defining things the right way.

I agree that this would be very close to more or less assuming the theorem. > I think that for a "proper" proof of it, > one should also show that Minkowski coincides with other measures of > "surface area", such as the length of a rectifiable curve in R^2, or the > surface integral for manifolds in higher dimensions (the latter of which > gets ugly as soon as you want to allow your objects to have sharp corners).

Mohammad

On 24/02/2021 17:39, Freek Wiedijk wrote:Hi Wenda,We may ask Freek for a longer list :-)Let's finish the first one first :-) That is: at least until we are at 99 theorems. When that happens, I would like to organise a workshop titled "I got 99 theorems, but Fermat ain't one"where I'll ask the most prolific contributors to the top100 list to present a talk. Freek

**Follow-Ups**:**Re: [isabelle] New in the AFP: Formal Puiseux Series***From:*Manuel Eberl

**Re: [isabelle] New in the AFP: Formal Puiseux Series***From:*Manuel Eberl

**References**:**[isabelle] New in the AFP: Formal Puiseux Series***From:*Lawrence Paulson

**Re: [isabelle] New in the AFP: Formal Puiseux Series***From:*Manuel Eberl

**Re: [isabelle] New in the AFP: Formal Puiseux Series***From:*Wenda Li

**Re: [isabelle] New in the AFP: Formal Puiseux Series***From:*Freek Wiedijk

**Re: [isabelle] New in the AFP: Formal Puiseux Series***From:*Manuel Eberl

- Previous by Date: [isabelle] Python client to Isabelle server
- Next by Date: Re: [isabelle] New in the AFP: Formal Puiseux Series
- Previous by Thread: Re: [isabelle] New in the AFP: Formal Puiseux Series
- Next by Thread: Re: [isabelle] New in the AFP: Formal Puiseux Series
- Cl-isabelle-users February 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list