Re: [isabelle] New in the AFP: Intersecting Chords Theorem



All of the ones that Johannes says can be proved by GrÃbner bases have been proved in HOL Light, which has well-developed GrÃbner basis algorithms. It would be interesting to see if the proofs make use of them.

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
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.