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

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?



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