*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:51:05 +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

I should probably add: there are also some problems (like "e is transcendental", "Ï is transcendental") that are perfectly within reach for a small side project for someone. The main reason why I haven't attacked them yet is that the proofs for those are a bit âad-hocâ. There are much stronger results like the very nice LindemannâWeierstraÃ theorem, which I'd very much like to see in Isabelle, but that is a bit more tricky to prove and I haven't found a nicely written-up version of it so far. As for the GrÃbner bases, I know very little about these things. We have some ML code doing something with GrÃbner basis, and we have the theoretical formalisation of them by Alexander Maletzky in the AFP. I don't know what would be required to use either of these to prove theorems like the ones you mentioned â that certainly sounds like an interesting idea though. Maybe one of our GrÃbner basis experts could comment on this? 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. >

**Follow-Ups**:**Re: [isabelle] New in the AFP: Intersecting Chords Theorem***From:*Tobias Nipkow

**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] finishing a proof
- 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