Lindemann–Weierstrass theorem (metamath 100 #56)

[digama0]

The Lindemann–Weierstrass theorem states that if if α1, ..., αn are algebraic numbers which are linearly independent over QQ, then e^α1, ..., e^αn are algebraically independent over QQ. Definitions df-aa and df-algind may be helpful in writing the statement. Metamath 100 theorem # 56.

• Blocks Metamath 100 theorem # 53 (pi is trancendental)
• Blocks Metamath 100 theorem # 67 (e is trancendental)

[david-a-wheeler]

I should note that no formalization system has, to my knowledge, proven this. Not even HOL light. That doesn't mean this cannot be done, indeed, it'd cool if it were done. Should this be deferred?

[david-a-wheeler]

Any progress on this?

[tirix]

A note that Andreas Sauer showed interest in the Hermite-Lindemann theorem on the mailing list, which is a special case of the Lindemann–Weierstrass theorem.

[avekens]

The Hermite-Lindemann Transcendence Theorem (Number 56 in "Formalizing 100 Theorems" by Freek Wiedijk: http://www.cs.ru.nl/%7Efreek/100/) is proven meanwhile by Coq and Isabelle:

• Coq, Sophie Bernard: https://madiot.fr/coq100/#56
• Isabelle, Manuel Eberl: http://www.cse.unsw.edu.au/~kleing/top100/#56

[david-a-wheeler]

@avekens - thanks for the more recent information. I'd love to see this proven in Metamath!

If someone proves it with Metamath, let me know so I can add it to our list of the Metamath 100.