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



As someone who has done quite a few of the Top 100 theorems in Isabelle,
I would say that the remaining ones fall mostly into three categories:

1. far too difficult to be done âjust for funâ
2. too far removed from what most Isabelle users are familiar with
3. too much underlying theory missing

or some linear combination thereof. I for one know very little about all
these geometric problems and have never really felt the appeal of
formalising them in Isabelle.

Still, there has been a pretty continuous trickle of problems of this
list being done in Isabelle in the past few years, and I am fairly
confident that this will continue.

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




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