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?
Cheers,
Manuel
On 13/10/16 18:08, Johannes Waldmann wrote: