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



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




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