*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] New in the AFP: Intersecting Chords Theorem*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Thu, 13 Oct 2016 18:33:11 +0200*In-reply-to*: <a698e11d-80b4-82c8-04cf-149399376cc5@htwk-leipzig.de>*References*: <a698e11d-80b4-82c8-04cf-149399376cc5@htwk-leipzig.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.3.0

As someone who has done quite a few of the Top 100 theorems in Isabelle, I would say that the remaining ones fall mostly into three categories: 1. far too difficult to be done âjust for funâ 2. too far removed from what most Isabelle users are familiar with 3. too much underlying theory missing or some linear combination thereof. I for one know very little about all these geometric problems and have never really felt the appeal of formalising them in Isabelle. Still, there has been a pretty continuous trickle of problems of this list being done in Isabelle in the past few years, and I am fairly confident that this will continue. Cheers, Manuel On 13/10/16 18:08, Johannes Waldmann wrote: >> ... the intersecting chords theorem. > > Yes, geometry is nice. > >> This theorem is the 55th theorem of the Top 100 Theorems list. > > So - what Isabelle formulations are missing - and why? > > Ok, I can compute the diff of http://www.cs.ru.nl/~freek/100/ > and http://www.cse.unsw.edu.au/~kleing/top100/ > but I'd be interested to know about the "why". > Is it mostly "too easy" or "too tedious" - > or is there something else, like "fundamentally hard"? > > The lowest-numbered items where Isabelle is missing, > but other systems have a formalisation, are > > 13 : Polyhedron Formula > 28 : Pascal's Hexagon Theorem > 29 : Feuerbach's Theorem > > I'm pretty sure 28 and 29 (and 61 - Ceva, 84 - Morley, 87 - Desargues) > can be proved automatically using computer algebra (with GrÃbner bases) > (cf. http://dx.doi.org/10.1016/S0747-7171(86)80006-2 ) > Of course, Isabelle is not a computer algebra system. > But you have https://www.isa-afp.org/entries/Groebner_Bases.shtml > so something could be done here. Well, I guess it's "why bother". > > - J. >

**References**:**Re: [isabelle] New in the AFP: Intersecting Chords Theorem***From:*Johannes Waldmann

- Previous by Date: Re: [isabelle] New in the AFP: Intersecting Chords Theorem
- Next by Date: Re: [isabelle] New in the AFP: Intersecting Chords Theorem
- Previous by Thread: Re: [isabelle] New in the AFP: Intersecting Chords Theorem
- Next by Thread: Re: [isabelle] New in the AFP: Intersecting Chords Theorem
- Cl-isabelle-users October 2016 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