Transcendence theory in Lean 4

15 References

Bak66

A. Baker, Linear forms in the logarithms of algebraic numbers I, Mathematika 13 (1966), 204–216.

Bak75

A. Baker, Transcendental Number Theory, Cambridge University Press, 1975.

BM80

D. Bertrand and D. W. Masser, Linear forms in elliptic integrals, Invent. Math. 58 (1980), 283–288.

Bro74

W. D. Brownawell, The algebraic independence of certain numbers related by the exponential function, J. Number Theory 6 (1974), 22–31.

DK24

S. Dasgupta and M. Kakde, Ranks of matrices of logarithms of algebraic numbers II: the Matrix Coefficient Conjecture, arXiv:2408.08178, 2024.

Gel34

A. O. Gel’fond, Sur le septième problème de Hilbert, Izv. Akad. Nauk SSSR (1934), 623–634.

Gel52

A. O. Gel’fond, Transcendental and Algebraic Numbers, 1952.

Her1873

C. Hermite, Sur la fonction exponentielle, C. R. Acad. Sci. Paris 77 (1873), 18–24, 74–79, 226–233, 285–293.

KW26

M. Karatarakis and F. Wiedijk, A formalization of the Gelfond–Schneider theorem, arXiv:2603.24823, 2026.

Lang66

S. Lang, Introduction to Transcendental Numbers, Addison-Wesley, 1966.

Lin1882

F. Lindemann, Über die Zahl \(\pi \), Math. Ann. 20 (1882), 213–225.

Mas81

D. W. Masser, A note on Baker’s theorem, in Recent Progress in Analytic Number Theory, Vol. 2 (Durham, 1979), Academic Press, 1981, 153–158.

Ram68

K. Ramachandra, Contributions to the theory of transcendental numbers I, Acta Arith. 14 (1968), 65–72.

RW95

D. Roy and M. Waldschmidt, Quadratic relations between logarithms of algebraic numbers, Proc. Japan Acad. Ser. A 71 (1995), 151–153.

RW97

D. Roy and M. Waldschmidt, Approximation diophantienne et indépendance algébrique de logarithmes, Ann. Sci. École Norm. Sup. (4) 30 (1997), 753–796.

Sch34

Th. Schneider, Transzendenzuntersuchungen periodischer Funktionen, J. Reine Angew. Math. 172 (1934), 65–69.

Sch57

Th. Schneider, Einführung in die transzendenten Zahlen, Springer, Berlin, 1957.

Tij71

R. Tijdeman, Proc. Kon. Nederl. Akad. Wetensch. Ser. A 74 (= Indag. Math. 33) (1971), 1–7.

Wal71

M. Waldschmidt, Indépendance algébrique des valeurs de la fonction exponentielle, Bull. Soc. Math. France 99 (1971), 285–304.

Wal73

M. Waldschmidt, Solution du huitième problème de Schneider, J. Number Theory 5 (1973), 191–202.

Wal00

M. Waldschmidt, Diophantine Approximation on Linear Algebraic Groups, Grundlehren der mathematischen Wissenschaften 326, Springer, 2000.

Wal09

M. Waldschmidt, Auxiliary functions in transcendence proofs, arXiv:0908.4024, 2009.

Wei1885

K. Weierstrass, Zu Lindemann’s Abhandlung “Über die Ludolph’sche Zahl”, Sitzungsber. Preuss. Akad. Wiss. (1885), 1067–1085.

Roy92

D. Roy, Matrices whose coefficients are linear forms in logarithms, J. Number Theory 41 (1992), 22–47.

Roy95

D. Roy, Points whose coordinates are logarithms of algebraic numbers on algebraic varieties, Acta Math. 175 (1995), 49–73.

Fis01

S. Fischler, Orbits under algebraic groups and logarithms of algebraic numbers, Acta Arith. 100 (2001), 167–187.

Dia07

G. Diaz, Produits et quotients de combinaisons linéaires de logarithmes de nombres algébriques : conjectures et résultats partiels, J. Théor. Nombres Bordeaux 19 (2007), 373–391.

Wal04

M. Waldschmidt, Open Diophantine problems, Mosc. Math. J. 4 (2004), 245–305.

Hat93

M. Hata, Rational approximations to the dilogarithm, Trans. Amer. Math. Soc. 336 (1993), 363–387.

RV05

G. Rhin and C. Viola, The permutation group method for the dilogarithm, Ann. Sc. Norm. Super. Pisa Cl. Sci. (5) 4 (2005), 389–437.

CDT24

F. Calegari, V. Dimitrov and Y. Tang, The linear independence of \(1\), \(\zeta (2)\), and \(L(2,\chi _{-3})\), arXiv:2408.15403, 2024.

Dia04

G. Diaz, Utilisation de la conjugaison complexe dans l’étude de la transcendance de valeurs de la fonction exponentielle usuelle, J. Théor. Nombres Bordeaux 16 (2004), 535–553.

BSZ17

C. Bachoc, O. Serra and G. Zémor, An analogue of Vosper’s theorem for extension fields, Math. Proc. Cambridge Philos. Soc. (2017); arXiv:1501.00602.

Kir18

J. Kirby, Variants of Schanuel’s conjecture, arXiv:1801.08765 (2018).