% Bibliography of paper.tex, for \bibliographystyle{amsplain}.
% Titles carry double braces because amsplain changes the case of a title otherwise.
% amsplain does not print the url field, so a link is also given in howpublished, which it does print.
% \lean is defined in the preamble of paper.tex.

% Checked 2026-11-05: Crossref doi:10.1006/jnth.1995.1088 gives vol. 53, no. 2, pp. 229--240.
@article{BosmaLenstra1995,
  author  = {W. Bosma and H. W. Lenstra},
  title   = {{Complete systems of two addition laws for elliptic curves}},
  journal = {J. Number Theory},
  volume  = {53},
  year    = {1995},
  pages   = {229--240},
}

@misc{ChCh26,
  author       = {G. V. Chudnovsky and D. V. Chudnovsky},
  title        = {{Irrationality exponents of real CM elliptic periods and powers of the lemniscate period}},
  howpublished = {arXiv:2610.31112},
  year         = {2026},
  note         = {with Lean files},
}

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

% Checked 2026-11-05 on the publisher's page (DROPS, doi:10.4230/LIPIcs.ITP.2026.23): peer-reviewed conference paper,
% Isabelle/HOL. The title previously recorded here ("Elliptic functions and modular forms in Isabelle/HOL") was wrong.
@inproceedings{EberlLiPaulson2026,
  author    = {M. Eberl and W. Li and L. C. Paulson},
  title     = {{From Weierstra\ss{} to Dedekind via Jacobi: formalising foundations of modular forms}},
  editor    = {E. Komendantskaya and T. Nipkow},
  booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
  series    = {LIPIcs},
  volume    = {382},
  publisher = {Schloss Dagstuhl},
  year      = {2026},
  pages     = {23:1--23:19},
}

@misc{KaratarakisWiedijk2026,
  author       = {M. Karatarakis and F. Wiedijk},
  title        = {{A formalization of the Gelfond--Schneider theorem}},
  howpublished = {arXiv:2603.24823},
  year         = {2026},
}

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

% Metadata from paper_cm/REFS_CHECK.md (zbMATH 0419.10035); the text of the note was not seen there.
@article{Laurent1980,
  author  = {M. Laurent},
  title   = {{Ind\'ependance lin\'eaire de valeurs de fonctions doublement quasi-p\'eriodiques}},
  journal = {C. R. Acad. Sci. Paris S\'er.~A},
  volume  = {290},
  year    = {1980},
  pages   = {397--399},
}

@inproceedings{Lean4,
  author    = {L. de Moura and S. Ullrich},
  title     = {{The Lean~4 theorem prover and programming language}},
  booktitle = {Automated Deduction -- CADE 28},
  series    = {Lecture Notes in Comput. Sci.},
  volume    = {12699},
  publisher = {Springer},
  year      = {2021},
  pages     = {625--635},
}

@misc{LeanMstar,
  author       = {Shawn Krisman},
  title        = {{four-exponentials-cm-periods}},
  howpublished = {\url{https://github.com/telaviv/four-exponentials-cm-periods}},
  url          = {https://github.com/telaviv/four-exponentials-cm-periods},
  year         = {2026},
  note         = {called \lean{lean_mstar} in this paper; library \lean{CM4E}, with this project as a Lake dependency},
}

@misc{LSGRepo,
  author       = {Shawn Krisman},
  title        = {{waldschmidt-subgroup-theorem}},
  howpublished = {\url{https://github.com/telaviv/waldschmidt-subgroup-theorem}},
  url          = {https://github.com/telaviv/waldschmidt-subgroup-theorem},
  year         = {2026},
}

@book{Masser1975,
  author    = {D. W. Masser},
  title     = {{Elliptic Functions and Transcendence}},
  series    = {Lecture Notes in Math.},
  volume    = {437},
  publisher = {Springer},
  year      = {1975},
}

% The publisher field holds the place as well: for this entry type amsplain prints address as the place of the conference.
@inproceedings{Mathlib,
  author    = {{The mathlib Community}},
  title     = {{The Lean mathematical library}},
  booktitle = {Proceedings of CPP 2020},
  publisher = {ACM, New York},
  year      = {2020},
  pages     = {367--381},
}

% Update when it has a preprint id.
@unpublished{MstarPaper,
  author = {Shawn Krisman},
  title  = {{A proof of the Roy--Waldschmidt theorem with period term, with explicit consequences at CM and Beta periods}},
  note   = {unrefereed draft, in the \lean{paper/} folder of \cite{LeanMstar}},
  year   = {2026},
}

@article{Philippon1986,
  author  = {P. Philippon},
  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. \textbf{115} (1987), 397--398},
}

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

@article{RoyWaldschmidt1993,
  author  = {D. Roy and M. Waldschmidt},
  title   = {{Autour du th\'eor\`eme du sous-groupe alg\'ebrique}},
  journal = {Canad. Math. Bull.},
  volume  = {36},
  year    = {1993},
  pages   = {358--367},
}

% Checked 2026-11-05: Crossref doi:10.1007/BF01571618 gives vol. 113, no. 1, pp. 1--13. (EuDML lists the pages as I--XIII.)
@article{Schneider1937,
  author  = {Th. Schneider},
  title   = {{Arithmetische Untersuchungen elliptischer Integrale}},
  journal = {Math. Ann.},
  volume  = {113},
  year    = {1937},
  pages   = {1--13},
}

@unpublished{StrongSixPaper,
  author = {Shawn Krisman},
  title  = {{A Lean formalization of Roy's strong six exponentials theorem}},
  note   = {preprint},
  year   = {2026},
}

@misc{StrongSixRepo,
  author       = {Shawn Krisman},
  title        = {{strong-six-exponentials}},
  howpublished = {\url{https://github.com/telaviv/strong-six-exponentials}},
  url          = {https://github.com/telaviv/strong-six-exponentials},
  year         = {2026},
}

@book{DALAG,
  author    = {M. Waldschmidt},
  title     = {{Diophantine Approximation on Linear Algebraic Groups}},
  series    = {Grundlehren Math. Wiss.},
  volume    = {326},
  publisher = {Springer},
  address   = {Berlin},
  year      = {2000},
  note      = {Chapters~5 and~8 by D.~Roy},
}

@article{W83,
  author  = {M. Waldschmidt},
  title   = {{Sous-groupes analytiques de groupes alg\'ebriques}},
  journal = {Ann. of Math. (2)},
  volume  = {117},
  year    = {1983},
  pages   = {627--657},
}

@incollection{W88,
  author    = {M. Waldschmidt},
  title     = {{On the transcendence methods of Gel'fond and Schneider in several variables}},
  editor    = {A. Baker},
  booktitle = {New Advances in Transcendence Theory (Durham, 1986)},
  publisher = {Cambridge Univ. Press},
  year      = {1988},
  pages     = {375--398},
}

@misc{WaldschmidtLIL,
  author       = {M. Waldschmidt},
  title        = {{Linear independence of logarithms of algebraic numbers}},
  howpublished = {IMSc Report 116, Madras},
  year         = {1992},
  note         = {revised 2016},
}

@article{Wustholz1989,
  author  = {G. W\"ustholz},
  title   = {{Algebraische Punkte auf analytischen Untergruppen algebraischer Gruppen}},
  journal = {Ann. of Math. (2)},
  volume  = {129},
  year    = {1989},
  pages   = {501--517},
}