Papers With

← All papers
First page of A formalization of the Gelfond-Schneider theorem

A formalization of the Gelfond-Schneider theorem

Michail Karatarakis, Freek Wiedijk

cs.LO Mar 25, 2026 · v1
formalization number-theory
Read PDF arXiv abstract
TL;DR
Formalizes Hilbert's Seventh Problem and the Gelfond-Schneider theorem in Lean 4.
Abstract
We formalize Hilbert's Seventh Problem and its solution, the Gelfond-Schneider theorem, in the Lean 4 proof assistant. The theorem states that if $α$ and $β$ are algebraic numbers with $α\neq 0,1$ and $β$ irrational, then $α^β$ is transcendental. Originally proven independently by Gelfond and Schneider in 1934, this result is a cornerstone of transcendental number theory, bridging algebraic number theory and complex analysis.
Problem

The Gelfond-Schneider theorem, which resolves Hilbert's Seventh Problem by establishing that alpha^beta is transcendental when alpha and beta are algebraic with alpha != 0,1 and beta irrational, had not been formally verified in a proof assistant.

Approach

The authors formalize the Gelfond-Schneider theorem in Lean 4 with Mathlib. The proof proceeds by constructing an auxiliary exponential polynomial R(z) that vanishes at lattice points, then deriving a contradiction between an arithmetic lower bound (from the house of an algebraic number and Siegel's lemma generalized to number field rings of integers) and an analytic upper bound (from complex analysis via a helper function S(z)). Key Lean developments include Siegel's lemma for algebraic integers, the house function, and bounds on auxiliary function derivatives.

Results

The full Gelfond-Schneider theorem is formalized in Lean 4, providing a machine-checked proof of the transcendence of alpha^beta under the classical hypotheses. The formalization includes new Mathlib contributions in algebraic number theory, including Siegel's lemma for rings of integers of number fields.