A formalization of the Gelfond-Schneider theorem

TL;DR

This paper formalizes the Gelfond-Schneider theorem within the Lean 4 proof assistant, providing a rigorous computer-verified proof of a fundamental result in transcendental number theory.

Contribution

It is the first formalization of the Gelfond-Schneider theorem, bridging algebraic number theory and complex analysis in a proof assistant.

Findings

Successful formalization in Lean 4

Verification of the theorem's proof correctness

Enhanced reproducibility of transcendental number theory results

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 $\alpha$ and $\beta$ are algebraic numbers with $\alpha \neq 0,1$ and $\beta$ irrational, then $\alpha^\beta$ 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.