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
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. )
Of course, Isabelle is not a computer algebra system.
But you have
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.