*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] New in the AFP: Intersecting Chords Theorem*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 14 Oct 2016 09:17:15 +0200*In-reply-to*: <92be815c-1412-d7a3-775f-37ef9323b9c1@in.tum.de>*References*: <a698e11d-80b4-82c8-04cf-149399376cc5@htwk-leipzig.de> <92be815c-1412-d7a3-775f-37ef9323b9c1@in.tum.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:45.0) Gecko/20100101 Thunderbird/45.4.0

Tobias On 13/10/2016 18:51, Manuel Eberl wrote:

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.

**Attachment:
smime.p7s**

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

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

**Re: [isabelle] New in the AFP: Intersecting Chords Theorem***From:*Manuel Eberl

- 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