@article{Roy1992,
  author  = {Roy, Damien},
  title   = {Matrices whose coefficients are linear forms in logarithms},
  journal = {J. Number Theory},
  volume  = {41},
  year    = {1992},
  pages   = {22--47}
}

@incollection{Waldschmidt1988,
  author    = {Waldschmidt, Michel},
  title     = {On the transcendence methods of {G}el'fond and {S}chneider in several variables},
  booktitle = {New Advances in Transcendence Theory ({D}urham, 1986)},
  editor    = {Baker, Alan},
  publisher = {Cambridge Univ. Press},
  address   = {Cambridge},
  year      = {1988},
  pages     = {375--398}
}

@book{DALAG,
  author    = {Waldschmidt, Michel},
  title     = {Diophantine Approximation on Linear Algebraic Groups},
  series    = {Grundlehren der Mathematischen Wissenschaften},
  volume    = {326},
  publisher = {Springer-Verlag},
  address   = {Berlin},
  year      = {2000},
  note      = {Chapters 5 and 8 by Damien Roy}
}

@article{Philippon1986,
  author  = {Philippon, Patrice},
  title   = {Lemmes de z\'eros dans les groupes alg\'ebriques commutatifs},
  journal = {Bull. Soc. Math. France},
  volume  = {114},
  year    = {1986},
  pages   = {355--383},
  note    = {Errata et addenda: ibid. 115 (1987), 397--398}
}

@article{Wustholz1989,
  author  = {W{\"u}stholz, Gisbert},
  title   = {Multiplicity estimates on group varieties},
  journal = {Ann. of Math. (2)},
  volume  = {129},
  year    = {1989},
  number  = {3},
  pages   = {471--500}
}

@article{Laurent1994,
  author  = {Laurent, Michel},
  title   = {Linear forms in two logarithms and interpolation determinants},
  journal = {Acta Arith.},
  volume  = {66},
  year    = {1994},
  number  = {2},
  pages   = {181--199}
}

@misc{WaldschmidtLIL,
  author       = {Waldschmidt, Michel},
  title        = {Linear independence of logarithms of algebraic numbers},
  howpublished = {IMSc Report 116, The Institute of Mathematical Sciences, Madras},
  year         = {1992},
  note         = {With an appendix by Michel Laurent. Revised version (2016) on the author's web page; chapter numbers refer to it}
}

@book{Lang1966,
  author    = {Lang, Serge},
  title     = {Introduction to Transcendental Numbers},
  publisher = {Addison-Wesley},
  address   = {Reading, MA},
  year      = {1966}
}

@article{Ramachandra1968,
  author  = {Ramachandra, K.},
  title   = {Contributions to the theory of transcendental numbers. {I}, {II}},
  journal = {Acta Arith.},
  volume  = {14},
  year    = {1967/68},
  pages   = {65--72, 73--88}
}

@book{Matsumura,
  author    = {Matsumura, Hideyuki},
  title     = {Commutative Ring Theory},
  series    = {Cambridge Studies in Advanced Mathematics},
  volume    = {8},
  publisher = {Cambridge Univ. Press},
  address   = {Cambridge},
  year      = {1986},
  note      = {Translated from the Japanese by M. Reid}
}

@misc{GuanHu2025,
  author       = {Guan, Nailin and Hu, Yongle},
  title        = {Formalization of {A}uslander--{B}uchsbaum--{S}erre criterion in {L}ean4},
  howpublished = {arXiv:2510.24818},
  year         = {2025}
}

@misc{KaratarakisWiedijk2026,
  author       = {Karatarakis, Michail and Wiedijk, Freek},
  title        = {A formalization of the {G}elfond--{S}chneider theorem},
  howpublished = {arXiv:2603.24823},
  year         = {2026}
}

@inproceedings{Lean4,
  author    = {de Moura, Leonardo and Ullrich, Sebastian},
  title     = {The {L}ean 4 Theorem Prover and Programming Language},
  booktitle = {Automated Deduction -- CADE 28},
  series    = {Lecture Notes in Computer Science},
  volume    = {12699},
  publisher = {Springer, Cham},
  year      = {2021},
  pages     = {625--635}
}

@inproceedings{Mathlib,
  author    = {{The mathlib Community}},
  title     = {The {L}ean Mathematical Library},
  booktitle = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020)},
  publisher = {Association for Computing Machinery},
  address   = {New York},
  year      = {2020},
  pages     = {367--381}
}

@misc{DiazModulus,
  author       = {Perassi, Carlo},
  title        = {diaz-modulus-lean: Transcendence theory in {L}ean 4},
  howpublished = {\url{https://github.com/carlok/diaz-modulus-lean}},
  year         = {2026},
  note         = {Accessed October 2026}
}