Congratulations! I had actually started down this road, managing to prove that the algebraic numbers were a field via linear combinations of powers (and coming up with an alternative proof of mreexexd to avoid AC), but when I realized that the proofs I needed would lean heavily on symmetric polynomials of roots of rational polynomials being rational I threw those out, since that fact would have gotten me there more quickly. I'm little surprised this is proven without pi, since I'd assumed that they'd come together, as a consequence of what I then planned to call "efnaa," but might be better now called "eftrans."
On Tuesday, April 7, 2020 at 4:20:07 PM UTC-4, David A. Wheeler wrote: > > I am very pleased to announce that the claim that e is Transcendental, > Metamath 100 #67, has been proven by Glauco in Metamath. This is another > tremendous achievement of his and I congratulate him. > > You can see the proof of ~ etransc here: > http://us.metamath.org/mpeuni/etransc.html > > The pull request (with discussion) is here: > https://github.com/metamath/set.mm/pull/1570 > > I've already modified the Metamath 100 list and its associated graph. > Later today I will send an email to Freek (who maintains the list for many > provers). > > This means that 74 / 100 challenge problems have been formally proven with > Metamath. With only 9 more, Metamath will tie Isabelle's current number > (83). You can see the list of what's left to do here: > http://us.metamath.org/mm_100.html#todo ... two related theorems are: > 53. π is Transcendental > 56. The Hermite-Lindemann Transcendence Theorem > > Again, congrats to Glauco! > > --- David A. Wheeler > -- 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/05e1a978-59d8-4ec0-a9e3-b073f37e6731%40googlegroups.com.
