Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Hermite–Lindemann gives all-integer phase independence

Proved
IntegerWindingExponentialIndependence.hermiteLindemannIntegerPhases

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

linear-algebranumber-theorytranscendencewinding

Assume the registered Hermite–Lindemann proposition. If α is a nonzero complex number algebraic over ℚ, then the family n ↦ exp(iαn), indexed by every integer n, is linearly independent over the field of complex algebraic numbers ℚ̄.

Preamble
import Definitions.Def_IntegerWindingExponentialIndependence_CoreV1
import Mathlib.FieldTheory.AlgebraicClosure
import Mathlib.Analysis.Complex.IsIntegral

set_option autoImplicit false
Formal statement
namespace IntegerWindingExponentialIndependence

theorem hermiteLindemannIntegerPhases
    (hHL : HermiteLindemann) (α : ℂ)
    (hα : IsAlgebraic ℚ α) (hα0 : α ≠ 0) :
    LinearIndependent (algebraicClosure ℚ ℂ)
      (fun n : ℤ => integerPhase (Complex.I * α) n) := by sorry

end IntegerWindingExponentialIndependence
Source
Javier Fresán, Gevrey Arithmetic and E-functions, Chapter 1, Theorem 1.1, https://javier.fresan.perso.math.cnrs.fr/gevrey.pdf; Encyclopedia of Mathematics, Lindemann theorem, https://encyclopediaofmath.org/wiki/Lindemann_theorem.
Read-back

What the Lean code literally says, in plain math · gpt-5.6-sol

Assume the proposition that, for every complex number β\betaβ, if β\betaβ is algebraic over Q\mathbb QQ and nonzero, then exp⁡(β)\exp(\beta)exp(β) is transcendental over Q\mathbb QQ. For every complex number α\alphaα that is algebraic over Q\mathbb QQ and satisfies α≠0\alpha\ne0α=0, the integer-indexed family (exp⁡ ⁣((n:C)(iα)))n∈Z\left(\exp\!\left((n:\mathbb C)(\mathrm i\alpha)\right)\right)_{n\in\mathbb Z}(exp((n:C)(iα)))n∈Z​ is linearly independent over the algebraic closure of Q\mathbb QQ inside C\mathbb CC. Explicitly, every finitely supported family of coefficients ana_nan​ from that algebraic closure which satisfies ∑n∈Zanexp⁡((n:C)(iα))=0\sum_{n\in\mathbb Z}a_n\exp((n:\mathbb C)(\mathrm i\alpha))=0∑n∈Z​an​exp((n:C)(iα))=0 has an=0a_n=0an​=0 for every nnn. The index set is all of Z\mathbb ZZ, including 000 and negative integers; the n=0n=0n=0 member is exp⁡(0)\exp(0)exp(0), while negative indices use negative integer multiples in the exponential. No assumption says that α\alphaα is real. The assertion is conditional on supplied proofs of the global exponential-transcendence proposition, algebraicity of α\alphaα, and α≠0\alpha\ne0α=0; when any required hypothesis is unavailable, the theorem supplies no conclusion for that case.

Human review
  • Endorsed by Shuze Chen · Sep 22, 2026

  • Endorsed by lisamegawatts · Sep 22, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me