A formalization of the Gelfond-Schneider theorem
This work provides a formal verification of a foundational theorem in mathematics, which is incremental as it applies an existing method to a known problem.
The authors formalized the Gelfond-Schneider theorem, a key result in transcendental number theory stating that under certain conditions, α^β is transcendental, using the Lean 4 proof assistant.
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.