2024.12.21 14:56:52 (Mastodon 113691394857507126, Twitter 1870483601969856831) from Daniel J. Bernstein:
HOL Light proof of the full Lindemann theorem (often incorrectly attributed to Weierstrass): https://cr.yp.to/2024/transcendence-20241221.ml The core of this proof follows 1990 Beukers--Bezivin--Robba rather than Hilbert. The symmetrization denouement is a simpler version of 1952 Steinberg--Redheffer.