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/
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".
This archive was generated by a fusion of
Pipermail (Mailman edition) and