A formalization of the Gelfond-Schneider theorem

arXiv:2603.24823v1 Announce Type: new
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.