1 Introduction
2 Tools ▶
3 Hermite–Lindemann and Lindemann–Weierstrass
4 Gelfond–Schneider
5 The six exponentials theorem
6 The four exponentials theorem in transcendence degree one ▶
7 Waldschmidt 1973 in full, and Schneider’s eighth problem ▶
- 7.1 One algebraic column
- 7.2 The theorems
8 Roy’s lemma
9 Baker’s theorem, by Schneider–Lang in several variables ▶
10 Rank-one configurations near a point of a circle ▶
11 A dichotomy for the dilogarithm at one half
12 Quadratic relations near a point of a circle ▶
13 Consequences in transcendence degree one ▶
14 Results not found in the sources read
15 References
Dependency graph

Transcendence theory in Lean 4

Carlo Perassi

Classical transcendence theory in Lean 4 and Mathlib, from Hermite–Lindemann to Baker’s theorem.

172 results
all proved
Lean’s three axioms

1 Introduction
2 Tools
3 Hermite–Lindemann and Lindemann–Weierstrass
4 Gelfond–Schneider
5 The six exponentials theorem
6 The four exponentials theorem in transcendence degree one
7 Waldschmidt 1973 in full, and Schneider’s eighth problem
- 7.1 One algebraic column
- 7.2 The theorems
8 Roy’s lemma
9 Baker’s theorem, by Schneider–Lang in several variables
10 Rank-one configurations near a point of a circle
11 A dichotomy for the dilogarithm at one half
12 Quadratic relations near a point of a circle
13 Consequences in transcendence degree one
14 Results not found in the sources read
15 References