Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | https://arxiv.org/abs/2603.24823 |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866915891697942528 |
|---|---|
| author | Karatarakis, Michail Wiedijk, Freek |
| author_facet | Karatarakis, Michail Wiedijk, Freek |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_24823 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A formalization of the Gelfond-Schneider theorem Karatarakis, Michail Wiedijk, Freek Logic in Computer Science 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. |
| title | A formalization of the Gelfond-Schneider theorem |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2603.24823 |