>They have relatively simple proofs of both these things relatively early on, how possible would it be to formalise these? Are proofs by contradiction difficult or impossible in metamath, are there any examples to copy?
It would be interesting to hear opinions of people who formalized theorems about transcendental numbers in metamath, but I think the proofs you referenced will be difficult to formalize not because they are proofs by contradiction, but because they implicitly use a lot of background material not present in set.mm. For example, both proofs use symmetric polynomials and some Galois theory (alg. conjugates in the first proof and embeddings of the field Q(d1, ..., ds) in the second). If I'm not mistaken, we don't even have a theorem proving that algebraic numbers form a ring in set.mm! -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/a5554894-d037-418f-93a6-c2338b4363ban%40googlegroups.com.
