Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] new in the AFP: The Transcendence of π

Email Gateway (Aug 22 2022 at 18:34):

From: Lawrence Paulson <lp15@cam.ac.uk>
Another day, another amazing AFP entry from Manuel Eberl:

"This entry shows the transcendence of π based on the classic proof using the fundamental theorem of symmetric polynomials first given by von Lindemann in 1882, but the formalisation mostly follows the version by Niven. The proof reuses much of the machinery developed in the AFP entry on the transcendence of e.”

You can download it here:

https://www.isa-afp.org/entries/Pi_Transcendental.html

Larry Paulson

Last updated: Apr 25 2024 at 12:23 UTC