Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A formalization of the Gelfond-Schneider theorem

Michail Karatarakis, Freek Wiedijk

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.

A formalization of the Gelfond-Schneider theorem

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 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.

Paper Structure

This paper contains 8 sections, 7 theorems, 40 equations.

Table of Contents

  1. Introduction
  2. Algebraic number theory
  3. The House of an Algebraic Number
  4. Siegel's Lemma for Number Fields
  5. Hilbert's seventh problem
  6. Step 1
  7. Discussion
  8. Conclusion

Key Result

Theorem 2

Let $0 < M < N$, and let $a_{jk}$ be rational integers satisfying $|a_{jk}| \leq A$, where $A \geq 1$, $1 \leq j \leq M$, and $1 \leq k \leq N.$ Then there exists a set of rational integers $x_1, \ldots, x_N$, not all zero, satisfying $a_{j1}x_1 + \cdots + a_{jN}x_N = 0$ for $1 \leq j \leq M,$ and $

Theorems & Definitions (8)

  • Definition 1
  • Theorem 2: Int.Matrix.exists_ne_zero_int_vec_norm_le'
  • Theorem 3
  • Theorem 4
  • Theorem 3.1: Gelfond-Schneider
  • Lemma 5
  • Theorem 6: exists_analyticOn_factor_R_at_add_one
  • Lemma 7