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/E1jLuhZ-0001WS-Fh%40rmmprod07.runbox.
