*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] New in the AFP: Formal Puiseux Series*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Fri, 26 Feb 2021 16:42:43 +0100*In-reply-to*: <20210224163900.soz2nd2babfbn4kl@xb27-stretch.fritz.box>*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>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.7.1

I think that's definitely in reach. The only two ones that are still missing are the "Fair Games Theorem" and the Isoperimetric Theorem. Not sure what "Fair Games" actually is, but my best guess is that it refers to the Optional Stopping Theorem. We do have a big amount of probability theory in Isabelle/HOL, and I think there is even some martingale theory in some AFP entry. The proof looks fairly simple, as long as the necessary background theory is there. The Isoperimetric Theorem is a bit more tricky because to even state it, one needs a way to talk about the perimeter of a set (or in higher dimensions, the "surface area"), and there are a number of different approaches, some of which are more general than others. The best approach, I think, would be to define the Minkowski measure and prove the Brunn–Minkowski inequality in R^n (all very doable with some basic measure theory; I even have some material about these things lying around somewhere already). The isoperimetric inequality for R^n in terms of the Minkowski measure follows very easily then. 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 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). Manuel 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 top > 100 list to present a talk. > > Freek >

**Attachment:
smime.p7s**

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

**Re: [isabelle] New in the AFP: Formal Puiseux Series***From:*Mohammad Abdulaziz

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

**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

- Previous by Date: [isabelle] Nitpick Codatatype - No Counterexample found
- 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