Hermite–Lindemann hypothesis discharged

Proved

IntegerWindingExponentialIndependence.hermiteLindemannProved

by lisamegawatts · Sep 19, 2026 · Mathlib c5ea003 (Lean v4.30.0)

lindemann-weierstrass-lean430-backportnumber-theorytranscendencewinding

The registered Hermite–Lindemann proposition is true: for every nonzero complex number $\beta$ algebraic over $\mathbb Q$ ,

e^{\beta}\text{ is transcendental over }\mathbb Q.

This theorem replaces the earlier conditional interface with a proved input.

Preamble

import Definitions.Def_IntegerWindingExponentialIndependence_CoreV1
import Mathlib.RingTheory.Localization.Integral

open IntegerWindingExponentialIndependence

Formal statement

theorem IntegerWindingExponentialIndependence.hermiteLindemannProved :
    HermiteLindemann := by sorry

Source

Consumes the proved Hermite--Lindemann theorem from Yuyang Zhao, mathlib4 PR #28013, https://github.com/leanprover-community/mathlib4/pull/28013, and the proved private mission Integer Winding Transcendence I: Exponential Phase Independence.

View graph