@Article{	  ABKNT_2024,
  title		= {Categorical foundations of formalized condensed
		  mathematics},
  doi		= {10.1017/jsl.2024.69},
  journal	= {The Journal of Symbolic Logic},
  author	= {Asgeirsson, Dagur and Brasca, Riccardo and Kuhn, Nikolas
		  and N{uccio Mortarino Majno di Capriglio}, Filippo A. E.
		  and Topaz, Adam},
  year		= {2024},
  pages		= {1-28},
  url		= {
		  https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/categorical-foundations-of-formalized-condensed-mathematics/0A003200BE44C4F78859DFAE19E3FFA8
		  }
}

@InProceedings{	  AGLST23,
  author	= {Avigad, Jeremy and Goldberg, Lior and Levit, David and
		  Seginer, Yoav and Titelman, Alon},
  title		= {{A Proof-Producing Compiler for Blockchain Applications}},
  booktitle	= {14th International Conference on Interactive Theorem
		  Proving (ITP 2023)},
  pages		= {7:1--7:19},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-284-6},
  issn		= {1868-8969},
  year		= {2023},
  volume	= {268},
  editor	= {Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/opus/volltexte/2023/18382},
  urn		= {urn:nbn:de:0030-drops-183820},
  doi		= {10.4230/LIPIcs.ITP.2023.7},
  annote	= {Keywords: formal verification, smart contracts,
		  interactive proof systems}
}

@InProceedings{	  AngdinataXu23,
  author	= {Angdinata, David Kurniadi and Xu, Junyan},
  title		= {{An Elementary Formal Proof of the Group Law on
		  Weierstrass Elliptic Curves in Any Characteristic}},
  booktitle	= {14th International Conference on Interactive Theorem
		  Proving (ITP 2023)},
  pages		= {6:1--6:19},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-284-6},
  issn		= {1868-8969},
  year		= {2023},
  volume	= {268},
  editor	= {Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/opus/volltexte/2023/18381},
  urn		= {urn:nbn:de:0030-drops-183817},
  doi		= {10.4230/LIPIcs.ITP.2023.6},
  annote	= {Keywords: formal math, algebraic geometry, elliptic curve,
		  group law, Lean, mathlib}
}

@InProceedings{	  Asgeirsson24,
  author	= {Asgeirsson, Dagur},
  title		= {{Towards Solid Abelian Groups: A Formal Proof of
		  N\"{o}beling’s Theorem}},
  booktitle	= {15th International Conference on Interactive Theorem
		  Proving (ITP 2024)},
  pages		= {6:1--6:17},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-337-9},
  issn		= {1868-8969},
  year		= {2024},
  volume	= {309},
  editor	= {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.6},
  urn		= {urn:nbn:de:0030-drops-207347},
  doi		= {10.4230/LIPIcs.ITP.2024.6},
  annote	= {Keywords: Condensed mathematics, N\"{o}beling’s theorem,
		  Lean, Mathlib, Interactive theorem proving}
}

@Book{		  Avig14,
  author	= "Avigad, Jeremy and {de Moura}, Leonardo and Kong, Soonho",
  title		= {{Theorem Proving in Lean}},
  year		= "2014",
  link		= "\url{https://lean-lang.org/tutorial/tutorial.pdf}",
  publisher	= "Carnegie Mellon University"
}

@Book{		  Avig17,
  author	= "Avigad, Jeremy and Lewis, Robert Y. and {van Doorn},
		  Floris",
  title		= {{Logic and Proof}},
  year		= "2017",
  link		= "\url{https://avigad.github.io/logic_and_proof}",
  publisher	= "Carnegie Mellon University"
}

@InProceedings{	  AvigadCarneiroHudon19,
  author	= {Jeremy Avigad and Mario M. Carneiro and Simon Hudon},
  title		= {Data Types as Quotients of Polynomial Functors},
  booktitle	= {10th International Conference on Interactive Theorem
		  Proving, {ITP} 2019, September 9-12, 2019, Portland, OR,
		  {USA}},
  pages		= {6:1--6:19},
  year		= {2019},
  url		= {https://doi.org/10.4230/LIPIcs.ITP.2019.6},
  doi		= {10.4230/LIPIcs.ITP.2019.6},
  timestamp	= {Fri, 27 Sep 2019 15:57:06 +0200},
  biburl	= {https://dblp.org/rec/conf/itp/AvigadCH19.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  Baanen20,
  author	= {Anne Baanen},
  editor	= {Nicolas Peltier and Viorica Sofronie{-}Stokkermans},
  title		= {A Lean Tactic for Normalising Ring Expressions with
		  Exponents (Short Paper)},
  booktitle	= {Automated Reasoning - 10th International Joint Conference,
		  {IJCAR} 2020, Paris, France, July 1-4, 2020, Proceedings,
		  Part {II}},
  series	= {Lecture Notes in Computer Science},
  volume	= {12167},
  pages		= {21--27},
  publisher	= {Springer},
  year		= {2020},
  url		= {https://doi.org/10.1007/978-3-030-51054-1\_2},
  doi		= {10.1007/978-3-030-51054-1\_2},
  timestamp	= {Thu, 06 Aug 2020 21:49:45 +0200},
  biburl	= {https://dblp.org/rec/conf/cade/Baanen20.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  Baanen22,
  author	= {Baanen, Anne},
  title		= {{Use and Abuse of Instance Parameters in the Lean
		  Mathematical Library}},
  booktitle	= {13th International Conference on Interactive Theorem
		  Proving (ITP 2022)},
  pages		= {4:1--4:20},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-252-5},
  issn		= {1868-8969},
  year		= {2022},
  volume	= {237},
  editor	= {Andronick, June and de Moura, Leonardo},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/opus/volltexte/2022/16713},
  urn		= {urn:nbn:de:0030-drops-167131},
  doi		= {10.4230/LIPIcs.ITP.2022.4},
  annote	= {Keywords: formalization of mathematics, dependent type
		  theory, typeclasses, algebraic hierarchy, Lean prover}
}

@InProceedings{	  BaanenBCD23,
  author	= {Anne Baanen and Alex J. Best and Nirvana Coppola and
		  Sander R. Dahmen},
  editor	= {Robbert Krebbers and Dmitriy Traytel and Brigitte Pientka
		  and Steve Zdancewic},
  title		= {Formalized Class Group Computations and Integral Points on
		  Mordell Elliptic Curves},
  booktitle	= {Proceedings of the 12th {ACM} {SIGPLAN} International
		  Conference on Certified Programs and Proofs, {CPP} 2023,
		  Boston, MA, USA, January 16-17, 2023},
  pages		= {47--62},
  publisher	= {{ACM}},
  year		= {2023},
  url		= {https://doi.org/10.1145/3573105.3575682},
  doi		= {10.1145/3573105.3575682},
  timestamp	= {Fri, 13 Jan 2023 13:05:42 +0100},
  biburl	= {https://dblp.org/rec/conf/cpp/BaanenBCD23.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  BaanenDahmenNarayananNuccio21,
  author	= {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni
		  and N{uccio Mortarino Majno di Capriglio}, Filippo A. E.},
  title		= {A Formalization of {D}edekind {D}omains an {C}lass
		  {G}roups of {G}lobal {F}ields},
  booktitle	= {12th International Conference on Interactive Theorem
		  Proving (ITP 2021)},
  pages		= {5:1--5:19},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-188-7},
  issn		= {1868-8969},
  year		= {2021},
  volume	= {193},
  editor	= {Cohen, Liron and Kaliszyk, Cezary},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.5},
  urn		= {urn:nbn:de:0030-drops-139004},
  doi		= {10.4230/LIPIcs.ITP.2021.5},
  annote	= {Keywords: formal math, algebraic number theory,
		  commutative algebra, Lean, mathlib}
}

@Article{	  BaanenDahmenNarayananNuccio22,
  author	= {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni
		  and N{uccio Mortarino Majno di Capriglio}, Filippo A. E.},
  title		= {A formalization of {D}edekind domains and class groups of
		  global fields},
  journal	= {J. Automat. Reason.},
  fjournal	= {Journal of Automated Reasoning},
  volume	= {66},
  year		= {2022},
  number	= {4},
  pages		= {611--637},
  issn		= {0168-7433,1573-0670},
  mrclass	= {03B35 (11R29 13C20)},
  mrnumber	= {4505023},
  doi		= {10.1007/s10817-022-09644-0},
  url		= {https://doi.org/10.1007/s10817-022-09644-0}
}

@InProceedings{	  BasoldBruinLawson24,
  author	= {Basold, Henning and Bruin, Peter and Lawson, Dominique},
  title		= {{The Directed Van Kampen Theorem in Lean}},
  booktitle	= {15th International Conference on Interactive Theorem
		  Proving (ITP 2024)},
  pages		= {8:1--8:18},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-337-9},
  issn		= {1868-8969},
  year		= {2024},
  volume	= {309},
  editor	= {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.8},
  urn		= {urn:nbn:de:0030-drops-207368},
  doi		= {10.4230/LIPIcs.ITP.2024.8},
  annote	= {Keywords: Lean, Directed Topology, Van Kampen Theorem,
		  Directed Homotopy Theory, Formalised Mathematics}
}

@Article{	  BBRBvY25,
  title		= {A complete formalization of Fermat's Last Theorem for
		  regular primes in Lean},
  author	= {Riccardo Brasca and Christopher Birkbeck and Eric
		  Rodriguez Boidi and Alex Best and Ruben van De Velde and
		  Andrew Yang},
  url		= {https://afm.episciences.org/14586},
  doi		= {10.46298/afm.14586},
  journal	= {Annals of Formalized Mathematics},
  volume	= {Volume 1},
  eid		= 4,
  year		= {2025},
  month		= {Jul},
  keywords	= {Lean, Mathlib, Kummer's lemma, [MATH.MATH-NT]Mathematics
		  [math]/Number Theory [math.NT], [INFO.INFO-LO]Computer
		  Science [cs]/Logic in Computer Science [cs.LO],
		  [INFO.INFO-FL]Computer Science [cs]/Formal Languages and
		  Automata Theory [cs.FL]},
  language	= {English}
}

@Booklet{	  Best2021,
  author	= {Alexander Best},
  title		= {Automatically Generalizing Theorems Using Typeclasses},
  howpublished	= {EasyChair Preprint no. 6216},
  url		= {https://easychair.org/publications/preprint/KLfT},
  year		= {2021}
}

@InProceedings{	  BestBirkbeckBrascaRodriguez23,
  author	= {Best, Alex J. and Birkbeck, Christopher and Brasca,
		  Riccardo and Rodriguez Boidi, Eric},
  title		= {{Fermat’s Last Theorem for Regular Primes}},
  booktitle	= {14th International Conference on Interactive Theorem
		  Proving (ITP 2023)},
  pages		= {36:1--36:8},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-284-6},
  issn		= {1868-8969},
  year		= {2023},
  volume	= {268},
  editor	= {Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/opus/volltexte/2023/18411},
  urn		= {urn:nbn:de:0030-drops-184115},
  doi		= {10.4230/LIPIcs.ITP.2023.36},
  annote	= {Keywords: Fermat’s Last Theorem, Cyclotomic fields,
		  Interactive theorem proving, Lean}
}

@InProceedings{	  BhatKeizerHughesGoensGrosser24,
  author	= {Bhat, Siddharth and Keizer, Alex and Hughes, Chris and
		  Goens, Andr\'{e}s and Grosser, Tobias},
  title		= {{Verifying Peephole Rewriting in SSA Compiler IRs}},
  booktitle	= {15th International Conference on Interactive Theorem
		  Proving (ITP 2024)},
  pages		= {9:1--9:20},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-337-9},
  issn		= {1868-8969},
  year		= {2024},
  volume	= {309},
  editor	= {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.9},
  urn		= {urn:nbn:de:0030-drops-207372},
  doi		= {10.4230/LIPIcs.ITP.2024.9},
  annote	= {Keywords: compilers, semantics, mechanization, MLIR, SSA,
		  regions, peephole rewrites}
}

@Article{	  BordgCavalleri2021,
  author	= {Anthony Bordg and Nicol{\`{o}} Cavalleri},
  title		= {Elements of Differential Geometry in Lean: {A} Report for
		  Mathematicians},
  journal	= {CoRR},
  volume	= {abs/2108.00484},
  year		= {2021},
  url		= {https://arxiv.org/abs/2108.00484},
  eprinttype	= {arXiv},
  eprint	= {2108.00484},
  timestamp	= {Thu, 05 Aug 2021 14:27:08 +0200},
  biburl	= {https://dblp.org/rec/journals/corr/abs-2108-00484.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Article{	  BrowningLutz22,
  author	= {Thomas Browning and Patrick Lutz},
  title		= {Formalizing Galois Theory},
  journal	= {Experimental Mathematics},
  volume	= {31},
  number	= {2},
  pages		= {413-424},
  year		= {2022},
  publisher	= {Taylor & Francis},
  doi		= {10.1080/10586458.2021.1986176},
  url		= {https://doi.org/10.1080/10586458.2021.1986176},
  eprint	= {https://doi.org/10.1080/10586458.2021.1986176}
}

@InProceedings{	  Buch18,
  author	= {Ulrik Buchholtz and Floris {van Doorn} and Egbert Rijke},
  title		= {Higher Groups in Homotopy Type Theory},
  booktitle	= {Proceedings of the 33rd Annual {ACM/IEEE} Symposium on
		  Logic in Computer Science, {LICS} 2018, Oxford, UK, July
		  09-12, 2018},
  pages		= {205--214},
  year		= {2018},
  crossref	= {DBLP:conf/lics/2018},
  url		= {https://doi.org/10.1145/3209108.3209150},
  doi		= {10.1145/3209108.3209150}
}

@InProceedings{	  BuzzardCommelinMassot20,
  author	= {Kevin Buzzard and Johan Commelin and Patrick Massot},
  title		= {Formalising perfectoid spaces},
  booktitle	= {Proceedings of the 9th {ACM} {SIGPLAN} International
		  Conference on Certified Programs and Proofs, {CPP} 2020,
		  New Orleans, LA, USA, January 20-21, 2020},
  pages		= {299--312},
  year		= {2020},
  url		= {https://doi.org/10.1145/3372885.3373830},
  doi		= {10.1145/3372885.3373830},
  timestamp	= {Thu, 23 Jan 2020 16:12:31 +0100},
  biburl	= {https://dblp.org/rec/conf/cpp/BuzzardCM20.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Article{	  BuzzardHLLFM21,
  author	= {Kevin Buzzard and Chris Hughes and Kenny Lau and Amelia
		  Livingston and Ramon Fern{\'{a}}ndez Mir and Scott
		  Morrison},
  title		= {Schemes in Lean},
  journal	= {Exp. Math.},
  volume	= {31},
  number	= {2},
  pages		= {355--363},
  year		= {2022},
  url		= {https://doi.org/10.1080/10586458.2021.1983489},
  doi		= {10.1080/10586458.2021.1983489},
  timestamp	= {Tue, 06 Dec 2022 13:15:09 +0100},
  biburl	= {https://dblp.org/rec/journals/em/BuzzardHLLMM22.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  Carneiro19,
  author	= {Mario M. Carneiro},
  title		= {Formalizing Computability Theory via Partial Recursive
		  Functions},
  booktitle	= {10th International Conference on Interactive Theorem
		  Proving, {ITP} 2019, September 9-12, 2019, Portland, OR,
		  {USA}},
  pages		= {12:1--12:17},
  year		= {2019},
  url		= {https://doi.org/10.4230/LIPIcs.ITP.2019.12},
  doi		= {10.4230/LIPIcs.ITP.2019.12},
  timestamp	= {Fri, 27 Sep 2019 15:57:06 +0200},
  biburl	= {https://dblp.org/rec/conf/itp/Carneiro19.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  carneiro_et_al:LIPIcs.ITP.2025.20,
  author	= {Carneiro, Mario and Riehl, Emily},
  title		= {{Formalizing Colimits in 𝒞at}},
  booktitle	= {16th International Conference on Interactive Theorem
		  Proving (ITP 2025)},
  year		= {2025},
  editor	= {Forster, Yannick and Keller, Chantal},
  volume	= {352},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  pages		= {20:1--20:19},
  address	= {Dagstuhl, Germany},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  annote	= {Keywords: category theory, infinity-category theory,
		  nerve, simplicial set, colimit},
  doi		= {10.4230/LIPIcs.ITP.2025.20},
  isbn		= {978-3-95977-396-6},
  issn		= {1868-8969},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.20},
  urn		= {urn:nbn:de:0030-drops-246186}
}

@Misc{		  CarneiroMaster,
  author	= {Mario Carneiro},
  title		= {The Type Theory of Lean},
  eprint	= {https://github.com/digama0/lean-type-theory/releases},
  note		= {Master thesis},
  year		= {2019},
  abstract	= {Meta-theoretic properties of Lean 3, including
		  soundness.}
}

@InProceedings{	  chambertloir_et_al:LIPIcs.ITP.2025.4,
  author	= {Chambert-Loir, Antoine and de Frutos-Fern\'{a}ndez,
		  Mar{\'\i}a In\'{e}s},
  title		= {{A Formalization of Divided Powers in Lean}},
  booktitle	= {16th International Conference on Interactive Theorem
		  Proving (ITP 2025)},
  year		= {2025},
  editor	= {Forster, Yannick and Keller, Chantal},
  volume	= {352},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  pages		= {4:1--4:17},
  address	= {Dagstuhl, Germany},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  annote	= {Keywords: Formal mathematics, algebraic number theory,
		  commutative algebra, divided powers, Lean, Mathlib},
  doi		= {10.4230/LIPIcs.ITP.2025.4},
  isbn		= {978-3-95977-396-6},
  issn		= {1868-8969},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.4},
  urn		= {urn:nbn:de:0030-drops-246038}
}

@InProceedings{	  Clune23,
  author	= {Joshua Clune},
  editor	= {Robbert Krebbers and Dmitriy Traytel and Brigitte Pientka
		  and Steve Zdancewic},
  title		= {A Formalized Reduction of Keller's Conjecture},
  booktitle	= {Proceedings of the 12th {ACM} {SIGPLAN} International
		  Conference on Certified Programs and Proofs, {CPP} 2023,
		  Boston, MA, USA, January 16-17, 2023},
  pages		= {90--101},
  publisher	= {{ACM}},
  year		= {2023},
  url		= {https://doi.org/10.1145/3573105.3575669},
  doi		= {10.1145/3573105.3575669},
  timestamp	= {Fri, 13 Jan 2023 13:05:42 +0100},
  biburl	= {https://dblp.org/rec/conf/cpp/Clune23.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  CluneQianBentkampAvigad24,
  author	= {Clune, Joshua and Qian, Yicheng and Bentkamp, Alexander
		  and Avigad, Jeremy},
  title		= {{Duper: A Proof-Producing Superposition Theorem Prover for
		  Dependent Type Theory}},
  booktitle	= {15th International Conference on Interactive Theorem
		  Proving (ITP 2024)},
  pages		= {10:1--10:20},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-337-9},
  issn		= {1868-8969},
  year		= {2024},
  volume	= {309},
  editor	= {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.10},
  urn		= {urn:nbn:de:0030-drops-207381},
  doi		= {10.4230/LIPIcs.ITP.2024.10},
  annote	= {Keywords: proof search, automatic theorem proving,
		  interactive theorem proving, Lean, dependent type theory}
}

@InProceedings{	  CommelinLewis21,
  author	= {Commelin, Johan and Lewis, Robert Y.},
  title		= {Formalizing the Ring of Witt Vectors},
  year		= {2021},
  isbn		= {9781450382991},
  publisher	= {Association for Computing Machinery},
  address	= {New York, NY, USA},
  url		= {https://doi.org/10.1145/3437992.3439919},
  doi		= {10.1145/3437992.3439919},
  abstract	= {The ring of Witt vectors W R over a base ring R is an
		  important tool in algebraic number theory and lies at the
		  foundations of modern p-adic Hodge theory. W R has the
		  interesting property that it constructs a ring of
		  characteristic 0 out of a ring of characteristic p > 1,
		  and it can be used more specifically to construct from a
		  finite field containing ℤ/pℤ the corresponding
		  unramified field extension of the p-adic numbers ℚp
		  (which is unique up to isomorphism). We formalize the
		  notion of a Witt vector in the Lean proof assistant, along
		  with the corresponding ring operations and other algebraic
		  structure. We prove in Lean that, for prime p, the ring of
		  Witt vectors over ℤ/pℤ is isomorphic to the ring of
		  p-adic integers ℤp. In the process we develop idioms to
		  cleanly handle calculations of identities between
		  operations on the ring of Witt vectors. These calculations
		  are intractable with a naive approach, and require a proof
		  technique that is usually skimmed over in the informal
		  literature. Our proofs resemble the informal arguments
		  while being fully rigorous.},
  booktitle	= {Proceedings of the 10th ACM SIGPLAN International
		  Conference on Certified Programs and Proofs},
  pages		= {264–277},
  numpages	= {14},
  keywords	= {ring theory, formal math, proof assistant, Lean, number
		  theory},
  location	= {Virtual, Denmark},
  series	= {CPP 2021}
}

@InProceedings{	  DahmenHolzlLewis19,
  author	= {Sander R. Dahmen and Johannes H{\"{o}}lzl and Robert Y.
		  Lewis},
  title		= {Formalizing the Solution to the Cap Set Problem},
  booktitle	= {10th International Conference on Interactive Theorem
		  Proving, {ITP} 2019, September 9-12, 2019, Portland, OR,
		  {USA}},
  pages		= {15:1--15:19},
  year		= {2019},
  url		= {https://doi.org/10.4230/LIPIcs.ITP.2019.15},
  doi		= {10.4230/LIPIcs.ITP.2019.15},
  timestamp	= {Mon, 23 Sep 2019 17:27:15 +0200},
  biburl	= {https://dblp.org/rec/conf/itp/DahmenHL19.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  deFrutos22,
  author	= {de Frutos-Fern\'{a}ndez, Mar{\'\i}a In\'{e}s},
  title		= {{Formalizing the Ring of Ad\`{e}les of a Global Field}},
  booktitle	= {13th International Conference on Interactive Theorem
		  Proving (ITP 2022)},
  pages		= {14:1--14:18},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-252-5},
  issn		= {1868-8969},
  year		= {2022},
  volume	= {237},
  editor	= {Andronick, June and de Moura, Leonardo},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/opus/volltexte/2022/16723},
  urn		= {urn:nbn:de:0030-drops-167232},
  doi		= {10.4230/LIPIcs.ITP.2022.14},
  annote	= {Keywords: formal math, algebraic number theory, class
		  field theory, Lean, mathlib}
}

@InProceedings{	  deFrutos23,
  author	= {de Frutos-Fern\'{a}ndez, Mar{\'\i}a In\'{e}s},
  title		= {{Formalizing Norm Extensions and Applications to Number
		  Theory}},
  booktitle	= {14th International Conference on Interactive Theorem
		  Proving (ITP 2023)},
  pages		= {13:1--13:18},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-284-6},
  issn		= {1868-8969},
  year		= {2023},
  volume	= {268},
  editor	= {Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/opus/volltexte/2023/18388},
  urn		= {urn:nbn:de:0030-drops-183880},
  doi		= {10.4230/LIPIcs.ITP.2023.13},
  annote	= {Keywords: formal mathematics, Lean, mathlib, algebraic
		  number theory, p-adic analysis, Galois representations,
		  p-adic Hodge theory}
}

@InProceedings{	  deFrutosNuccio24,
  author	= {de Frutos-Fern\'{a}ndez, Mar\'{\i}a In\'{e}s and N{uccio
		  Mortarino Majno di Capriglio}, Filippo A. E.},
  title		= {A Formalization of Complete Discrete Valuation Rings and
		  Local Fields},
  year		= {2024},
  isbn		= {9798400704888},
  publisher	= {Association for Computing Machinery},
  address	= {New York, NY, USA},
  url		= {https://doi.org/10.1145/3636501.3636942},
  doi		= {10.1145/3636501.3636942},
  abstract	= {Local fields, and fields complete with respect to a
		  discrete valuation, are essential objects in commutative
		  algebra, with applications to number theory and algebraic
		  geometry. We formalize in Lean the basic theory of
		  discretely valued fields. In particular, we prove that the
		  unit ball with respect to a discrete valuation on a field
		  is a discrete valuation ring and, conversely, that the adic
		  valuation on the field of fractions of a discrete valuation
		  ring is discrete. We define finite extensions of valuations
		  and of discrete valuation rings, and prove some
		  localization results. Building on this general theory, we
		  formalize the abstract definition and some fundamental
		  properties of local fields. As an application, we show that
		  finite extensions of the field ℚp of p-adic numbers and
		  of the field Fp((X)) of Laurent series over Fp are local
		  fields.},
  booktitle	= {Proceedings of the 13th ACM SIGPLAN International
		  Conference on Certified Programs and Proofs {(CPP '24)}},
  pages		= {190–204},
  numpages	= {15},
  keywords	= {mathlib, local fields, formal mathematics, discrete
		  valuation rings, algebraic number theory, Lean},
  series	= {CPP 2024}
}

@Misc{		  DeMoura15,
  author	= "{de Moura}, Leonardo and Avigad, Jeremy and Kong, Soonho
		  and Roux, Cody",
  title		= {{Elaboration in Dependent Type Theory}},
  link		= "\url{https://arxiv.org/pdf/1505.04324.pdf}",
  year		= "2015",
  abstract	= {Elaboration in Lean 2}
}

@InProceedings{	  DeMouraKongAvigadVanDoornvonRaumer,
  author	= {Leonardo Mendonça {de Moura} and Soonho Kong and Jeremy
		  Avigad and Floris {van Doorn} and Jakob {von Raumer}},
  title		= {The Lean Theorem Prover (System Description)},
  booktitle	= {Automated Deduction - CADE-25 - 25th International
		  Conference on Automated Deduction, Berlin, Germany, August
		  1-7, 2015, Proceedings},
  pages		= {378--388},
  year		= {2015},
  crossref	= {DBLP:conf/cade/2015},
  url		= "\url{https://doi.org/10.1007/978-3-319-21401-6_26}",
  doi		= {10.1007/978-3-319-21401-6\_26},
  timestamp	= {Tue, 14 May 2019 10:00:39 +0200},
  biburl	= {https://dblp.org/rec/conf/cade/MouraKADR15.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org},
  abstract	= {System description of Lean 2}
}

@InProceedings{	  deMouraUllrich2021,
  author	= "Moura, Leonardo de and Ullrich, Sebastian",
  editor	= "Platzer, Andr{\'e} and Sutcliffe, Geoff",
  title		= "The Lean 4 Theorem Prover and Programming Language",
  booktitle	= "Automated Deduction -- CADE 28",
  year		= "2021",
  publisher	= "Springer International Publishing",
  address	= "Cham",
  pages		= "625--635",
  abstract	= "Lean 4 is a reimplementation of the Lean interactive
		  theorem prover (ITP) in Lean itself. It addresses many
		  shortcomings of the previous versions and contains many new
		  features. Lean 4 is fully extensible: users can modify and
		  extend the parser, elaborator, tactics, decision
		  procedures, pretty printer, and code generator. The new
		  system has a hygienic macro system custom-built for ITPs.
		  It contains a new typeclass resolution procedure based on
		  tabled resolution, addressing significant performance
		  problems reported by the growing user base. Lean 4 is also
		  an efficient functional programming language based on a
		  novel programming paradigm called functional but in-place.
		  Efficient code generation is crucial for Lean users because
		  many write custom proof automation procedures in Lean
		  itself.",
  isbn		= "978-3-030-79876-5",
  url		= {https://link.springer.com/chapter/10.1007/978-3-030-79876-5_37}
}

@InProceedings{	  DilliesMehta22,
  author	= {Dillies, Ya\"{e}l and Mehta, Bhavik},
  title		= {{Formalising Szemer\'{e}di’s Regularity Lemma in Lean}},
  booktitle	= {13th International Conference on Interactive Theorem
		  Proving (ITP 2022)},
  pages		= {9:1--9:19},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-252-5},
  issn		= {1868-8969},
  year		= {2022},
  volume	= {237},
  editor	= {Andronick, June and de Moura, Leonardo},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/opus/volltexte/2022/16718},
  urn		= {urn:nbn:de:0030-drops-167185},
  doi		= {10.4230/LIPIcs.ITP.2022.9},
  annote	= {Keywords: Lean, formalisation, formal proof, graph theory,
		  combinatorics, additive combinatorics, Szemer\'{e}di’s
		  Regularity Lemma, Roth’s Theorem}
}

@InProceedings{	  Door16,
  author	= {Floris {van Doorn}},
  title		= {Constructing the propositional truncation using
		  non-recursive HITs},
  booktitle	= {Proceedings of the 5th {ACM} {SIGPLAN} Conference on
		  Certified Programs and Proofs, Saint Petersburg, FL, USA,
		  January 20-22, 2016},
  pages		= {122--129},
  year		= {2016},
  crossref	= {DBLP:conf/cpp/2016},
  url		= {https://doi.org/10.1145/2854065.2854076},
  doi		= {10.1145/2854065.2854076},
  timestamp	= {Tue, 06 Nov 2018 16:59:23 +0100},
  biburl	= {https://dblp.org/rec/bib/conf/cpp/Doorn16},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  Door17,
  author	= {Floris {van Doorn} and Jakob {von Raumer} and Ulrik
		  Buchholtz},
  title		= {Homotopy Type Theory in Lean},
  booktitle	= {Interactive Theorem Proving - 8th International
		  Conference, {ITP} 2017, Bras{\'{\i}}lia, Brazil, September
		  26-29, 2017, Proceedings},
  pages		= {479--495},
  year		= {2017},
  crossref	= {DBLP:conf/itp/2017},
  url		= "\url{https://doi.org/10.1007/978-3-319-66107-0_30}",
  doi		= {10.1007/978-3-319-66107-0\_30},
  timestamp	= {Tue, 14 May 2019 10:00:37 +0200},
  biburl	= {https://dblp.org/rec/bib/conf/itp/DoornRB17},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  Door21,
  author	= {Floris {van Doorn}},
  title		= {{Formalized Haar Measure}},
  booktitle	= {12th International Conference on Interactive Theorem
		  Proving (ITP 2021)},
  pages		= {18:1--18:17},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-188-7},
  issn		= {1868-8969},
  year		= {2021},
  volume	= {193},
  editor	= {Cohen, Liron and Kaliszyk, Cezary},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/opus/volltexte/2021/13913},
  urn		= {urn:nbn:de:0030-drops-139139},
  doi		= {10.4230/LIPIcs.ITP.2021.18},
  annote	= {Keywords: Haar measure, measure theory, Bochner integral,
		  Lean, interactive theorem proving, formalized mathematics}
}

@InProceedings{	  DoornMN23,
  author	= {Floris van Doorn and Patrick Massot and Oliver Nash},
  editor	= {Robbert Krebbers and Dmitriy Traytel and Brigitte Pientka
		  and Steve Zdancewic},
  title		= {Formalising the h-Principle and Sphere Eversion},
  booktitle	= {Proceedings of the 12th {ACM} {SIGPLAN} International
		  Conference on Certified Programs and Proofs, {CPP} 2023,
		  Boston, MA, USA, January 16-17, 2023},
  pages		= {121--134},
  publisher	= {{ACM}},
  year		= {2023},
  url		= {https://doi.org/10.1145/3573105.3575688},
  doi		= {10.1145/3573105.3575688},
  timestamp	= {Fri, 13 Jan 2023 13:05:42 +0100},
  biburl	= {https://dblp.org/rec/conf/cpp/DoornMN23.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Article{	  DupuisLewisMacbeth22,
  author	= {Dupuis, Fr\'{e}d\'{e}ric and Lewis, Robert Y. and Macbeth,
		  Heather},
  title		= {{Formalized functional analysis with semilinear maps}},
  booktitle	= {13th International Conference on Interactive Theorem
		  Proving (ITP 2022)},
  pages		= {10:1--10:19},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-252-5},
  issn		= {1868-8969},
  year		= {2022},
  volume	= {237},
  editor	= {Andronick, June and de Moura, Leonardo},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/opus/volltexte/2022/16719},
  urn		= {urn:nbn:de:0030-drops-167191},
  doi		= {10.4230/LIPIcs.ITP.2022.10},
  annote	= {Keywords: Functional analysis, Lean, linear algebra,
		  semilinear, Hilbert space}
}

@InProceedings{	  dvorak_et_al:LIPIcs.ITP.2023.15,
  author	= {Dvorak, Martin and Blanchette, Jasmin},
  title		= {{Closure Properties of General Grammars – Formally
		  Verified}},
  booktitle	= {14th International Conference on Interactive Theorem
		  Proving (ITP 2023)},
  pages		= {15:1--15:16},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-284-6},
  issn		= {1868-8969},
  year		= {2023},
  volume	= {268},
  editor	= {Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.15},
  urn		= {urn:nbn:de:0030-drops-183906},
  doi		= {10.4230/LIPIcs.ITP.2023.15},
  annote	= {Keywords: Lean, type-0 grammars, recursively enumerable
		  languages, Kleene star}
}

@Article{	  EURAM17,
  author	= {Gabriel Ebner and Sebastian Ullrich and Jared Roesch and
		  Jeremy Avigad and Leonardo {de Moura}},
  title		= {A metaprogramming framework for formal verification},
  journal	= {{PACMPL}},
  volume	= {1},
  number	= {{ICFP}},
  pages		= {34:1--34:29},
  year		= {2017},
  url		= {https://doi.org/10.1145/3110278},
  doi		= {10.1145/3110278},
  timestamp	= {Tue, 06 Nov 2018 12:51:05 +0100},
  biburl	= {https://dblp.org/rec/bib/journals/pacmpl/EbnerURAM17},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  Ezeh24,
  author	= {Ezeh, Sam},
  title		= {{Graphical Rewriting for Diagrammatic Reasoning in
		  Monoidal Categories in Lean4}},
  booktitle	= {15th International Conference on Interactive Theorem
		  Proving (ITP 2024)},
  pages		= {41:1--41:8},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-337-9},
  issn		= {1868-8969},
  year		= {2024},
  volume	= {309},
  editor	= {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.41},
  urn		= {urn:nbn:de:0030-drops-207690},
  doi		= {10.4230/LIPIcs.ITP.2024.41},
  annote	= {Keywords: Interactive theorem proving, Lean4, Graphical
		  User Interface}
}

@Misc{		  FernandezMir19,
  author	= {Ramon Fernández Mir},
  title		= {Schemes in Lean},
  eprint	= {https://www.imperial.ac.uk/media/imperial-college/faculty-of-engineering/computing/public/1819-ug-projects/Fernandez-I-MirR-Schemes-in-Lean.pdf},
  note		= {Project report},
  year		= {2019}
}

@InProceedings{	  gandhi_et_al:LIPIcs.ITP.2025.12,
  author	= {Gandhi, Anshula and Tadipatri, Anand Rao and Gowers,
		  Timothy},
  title		= {{Automatically Generalizing Proofs and Statements}},
  booktitle	= {16th International Conference on Interactive Theorem
		  Proving (ITP 2025)},
  year		= {2025},
  editor	= {Forster, Yannick and Keller, Chantal},
  volume	= {352},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  pages		= {12:1--12:18},
  address	= {Dagstuhl, Germany},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  annote	= {Keywords: automated reasoning, automated theorem proving,
		  interactive theorem proving, formalization of mathematics,
		  generalization, Lean theorem prover, Lean tactic},
  doi		= {10.4230/LIPIcs.ITP.2025.12},
  isbn		= {978-3-95977-396-6},
  issn		= {1868-8969},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.12},
  urn		= {urn:nbn:de:0030-drops-246104}
}

@Article{	  Gouezel2021,
  author	= {S{\'{e}}bastien Gou{\"{e}}zel},
  title		= {Formalizing the Gromov-Hausdorff space},
  journal	= {CoRR},
  volume	= {abs/2108.13660},
  year		= {2021},
  url		= {https://arxiv.org/abs/2108.13660},
  eprinttype	= {arXiv},
  eprint	= {2108.13660},
  timestamp	= {Fri, 03 Sep 2021 10:51:17 +0200},
  biburl	= {https://dblp.org/rec/journals/corr/abs-2108-13660.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  Gouezel22,
  author	= {S{\'{e}}bastien Gou{\"{e}}zel},
  editor	= {Kevin Buzzard and Temur Kutsia},
  title		= {A Formalization of the Change of Variables Formula for
		  Integrals in mathlib},
  booktitle	= {Intelligent Computer Mathematics - 15th International
		  Conference, {CICM} 2022, Tbilisi, Georgia, September 19-23,
		  2022, Proceedings},
  series	= {Lecture Notes in Computer Science},
  volume	= {13467},
  pages		= {3--18},
  publisher	= {Springer},
  year		= {2022},
  url		= {https://doi.org/10.1007/978-3-031-16681-5\_1},
  doi		= {10.1007/978-3-031-16681-5\_1},
  timestamp	= {Mon, 19 Sep 2022 18:41:40 +0200},
  biburl	= {https://dblp.org/rec/conf/mkm/Gouezel22.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  GrowingMathlib,
  author	= {Baanen, Anne and Ballard, Matthew Robert and Commelin,
		  Johan and Chen, Bryan Gin--ge and Rothgang, Michael and
		  Testa, Damiano},
  title		= {Growing Mathlib: maintenance of a large scale mathematical
		  library},
  booktitle	= {Intelligent Computer Mathematics},
  year		= {2026},
  editor	= {de Paiva, Valeria and Koepke, Peter},
  publisher	= {Springer Nature Switzerland},
  isbn		= {978-3-032-07021-0},
  pages		= {51--70},
  abstract	= {The Lean mathematical library Mathlib is one of the
		  fastest-growing libraries of formalised mathematics. We
		  describe various strategies to manage this growth, while
		  allowing for change and avoiding maintainer overload. This
		  includes dealing with breaking changes via a deprecation
		  system, using code quality analysis tools (linters) to
		  provide direct user feedback about common pitfalls,
		  speeding up compilation times through conscious library
		  (re-)design, dealing with technical debt as well as writing
		  custom tooling to help with the review and triage of new
		  contributions.},
  address	= {Cham},
  url		= {https://link.springer.com/chapter/10.1007/978-3-032-07021-0_4},
  doi		= {10.1007/978-3-032-07021-0_4}
}

@Misc{		  GusakovMehtaMiller21,
  title		= {Formalizing Hall's Marriage Theorem in Lean},
  author	= {Alena Gusakov and Bhavik Mehta and Kyle A. Miller},
  year		= {2021},
  eprint	= {2101.00127},
  archiveprefix	= {arXiv},
  primaryclass	= {math.CO},
  url		= {https://arxiv.org/abs/2101.00127}
}

@InProceedings{	  HanVanDoorn,
  author	= {Jesse Michael Han and Floris {van Doorn}},
  title		= {A formal proof of the independence of the continuum
		  hypothesis},
  booktitle	= {Proceedings of the 9th {ACM} {SIGPLAN} International
		  Conference on Certified Programs and Proofs, {CPP} 2020,
		  New Orleans, LA, USA, January 20-21, 2020},
  pages		= {353--366},
  year		= {2020},
  url		= {https://doi.org/10.1145/3372885.3373826},
  doi		= {10.1145/3372885.3373826},
  timestamp	= {Thu, 23 Jan 2020 16:12:31 +0100},
  biburl	= {https://dblp.org/rec/conf/cpp/HanD20.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  HanVanDoorn19,
  author	= {Jesse Michael Han and Floris {van Doorn}},
  title		= {A Formalization of Forcing and the Unprovability of the
		  Continuum Hypothesis},
  booktitle	= {10th International Conference on Interactive Theorem
		  Proving, {ITP} 2019, September 9-12, 2019, Portland, OR,
		  {USA}},
  pages		= {19:1--19:19},
  year		= {2019},
  crossref	= {DBLP:conf/itp/2019},
  url		= {https://doi.org/10.4230/LIPIcs.ITP.2019.19},
  doi		= {10.4230/LIPIcs.ITP.2019.19},
  timestamp	= {Sat, 07 Sep 2019 02:31:13 +0200},
  biburl	= {https://dblp.org/rec/conf/itp/HanD19.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Misc{		  Huisinga19,
  author	= {Marc Huisinga},
  title		= {Formally Verified Insertion of Reference Counting
		  Instructions},
  eprint	= {https://pp.ipd.kit.edu/uploads/publikationen/huisinga19bachelorarbeit.pdf},
  note		= {Bachelor thesis},
  year		= {2019}
}

@InCollection{	  KjosHanssenNiraulaYoon22,
  author	= {Kjos-Hanssen, Bj{\o}rn and Niraula, Saroj and Yoon,
		  Soowhan},
  title		= {A parametrized family of {T}versky metrics connecting the
		  {J}accard distance to an analogue of the normalized
		  information distance},
  booktitle	= {L{FCS}: Logical foundations of computer science},
  series	= {Lecture Notes in Comput. Sci.},
  publisher	= {Springer, [Cham]},
  url		= {https://arxiv.org/abs/2111.02498},
  year		= {2022}
}

@Booklet{	  Kudryashov2021,
  author	= {Yury Kudryashov},
  title		= {Formalizing Rotation Number and Its Properties in Lean},
  howpublished	= {EasyChair Preprint no. 6168},
  url		= {https://easychair.org/publications/preprint/38w1},
  year		= {2021}
}

@InProceedings{	  Kudryashov22,
  author	= {Kudryashov, Yury},
  title		= {{Formalizing the Divergence Theorem and the Cauchy
		  Integral Formula in Lean}},
  booktitle	= {13th International Conference on Interactive Theorem
		  Proving (ITP 2022)},
  pages		= {23:1--23:19},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-252-5},
  issn		= {1868-8969},
  year		= {2022},
  volume	= {237},
  editor	= {Andronick, June and de Moura, Leonardo},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/opus/volltexte/2022/16732},
  urn		= {urn:nbn:de:0030-drops-167326},
  doi		= {10.4230/LIPIcs.ITP.2022.23},
  annote	= {Keywords: divergence theorem, Green’s theorem, Gauge
		  integral, Cauchy integral formula, Cauchy-Goursat theorem,
		  complex analysis}
}

@InProceedings{	  LeeHurLopes19,
  author	= {Juneyoung Lee and Chung{-}Kil Hur and Nuno P. Lopes},
  title		= {AliveInLean: {A} Verified {LLVM} Peephole Optimization
		  Verifier},
  booktitle	= {Computer Aided Verification - 31st International
		  Conference, {CAV} 2019, New York City, NY, USA, July 15-18,
		  2019, Proceedings, Part {II}},
  pages		= {445--455},
  year		= {2019},
  url		= "\url{https://doi.org/10.1007/978-3-030-25543-5_25}",
  doi		= {10.1007/978-3-030-25543-5\_25},
  timestamp	= {Fri, 27 Mar 2020 08:45:57 +0100},
  biburl	= {https://dblp.org/rec/conf/cav/LeeHL19.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  Lewis17,
  author	= {Robert Y. Lewis},
  title		= {An Extensible Ad Hoc Interface between Lean and
		  Mathematica},
  booktitle	= {Proceedings of the Fifth Workshop on Proof eXchange for
		  Theorem Proving, PxTP 2017, Bras{\'{\i}}lia, Brazil, 23-24
		  September 2017},
  pages		= {23--37},
  year		= {2017},
  url		= {https://doi.org/10.4204/EPTCS.262.4},
  doi		= {10.4204/EPTCS.262.4},
  timestamp	= {Wed, 12 Sep 2018 01:05:13 +0200},
  biburl	= {https://dblp.org/rec/journals/corr/abs-1712-09288.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  Lewis19,
  author	= {Robert Y. Lewis},
  title		= {A formal proof of {H}ensel's lemma over the p-adic
		  integers},
  booktitle	= {Proceedings of the 8th {ACM} {SIGPLAN} International
		  Conference on Certified Programs and Proofs, {CPP} 2019,
		  Cascais, Portugal, January 14-15, 2019},
  pages		= {15--26},
  year		= {2019},
  crossref	= {DBLP:conf/cpp/2019},
  url		= {https://doi.org/10.1145/3293880.3294089},
  doi		= {10.1145/3293880.3294089},
  timestamp	= {Fri, 04 Jan 2019 10:46:45 +0100},
  biburl	= {https://dblp.org/rec/bib/conf/cpp/Lewis19},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  LewisMadelaine20,
  author	= {Robert Y. Lewis and Paul{-}Nicolas Madelaine},
  title		= {Simplifying Casts and Coercions},
  booktitle	= {Practical Aspects of Automated Reasoning, {PAAR} 2020},
  year		= {2020},
  url		= {https://arxiv.org/abs/2001.10594},
  archiveprefix	= {arXiv},
  eprint	= {2001.10594},
  timestamp	= {Thu, 30 Jan 2020 18:46:36 +0100},
  biburl	= {https://dblp.org/rec/journals/corr/abs-2001-10594.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Article{	  LewisWu22,
  author	= {Robert Y. Lewis and Minchao Wu},
  title		= {A bi-directional extensible interface between Lean and
		  Mathematica},
  journal	= {{Journal of Automated Reasoning}},
  volume	= {66},
  number	= {1},
  year		= {2022},
  url		= {https://robertylewis.com/leanmm/lean_mm.pdf},
  doi		= {https://doi.org/10.1007/s10817-021-09611-1}
}

@InProceedings{	  Limperg21,
  author	= {Limperg, Jannis},
  title		= {A Novice-Friendly Induction Tactic for Lean},
  year		= {2021},
  isbn		= {9781450382991},
  publisher	= {Association for Computing Machinery},
  address	= {New York, NY, USA},
  url		= {https://doi.org/10.1145/3437992.3439928},
  doi		= {10.1145/3437992.3439928},
  abstract	= {In theorem provers based on dependent type theory such as
		  Coq and Lean, induction is a fundamental proof method and
		  induction tactics are omnipresent in proof scripts. Yet the
		  ergonomics of existing induction tactics are not ideal:
		  they do not reliably support inductive predicates and
		  relations; they sometimes generate overly specific or
		  unnecessarily complex induction hypotheses; and they
		  occasionally choose confusing names for the hypotheses they
		  introduce. This paper describes a new induction tactic,
		  implemented in Lean 3, which addresses these issues. The
		  tactic is particularly suitable for educational use, but
		  experts should also find it more convenient than existing
		  induction tactics. In addition, the tactic serves as a
		  moderately complex case study for the metaprogramming
		  framework of Lean 3. The paper describes some difficulties
		  encountered during the implementation and suggests
		  improvements to the framework.},
  booktitle	= {Proceedings of the 10th ACM SIGPLAN International
		  Conference on Certified Programs and Proofs},
  pages		= {199–211},
  numpages	= {13},
  keywords	= {induction, Lean, tactic, type theory, metaprogramming},
  location	= {Virtual, Denmark},
  series	= {CPP 2021}
}

@InProceedings{	  LimpergF23,
  author	= {Jannis Limperg and Asta Halkj{\ae}r From},
  editor	= {Robbert Krebbers and Dmitriy Traytel and Brigitte Pientka
		  and Steve Zdancewic},
  title		= {Aesop: White-Box Best-First Proof Search for Lean},
  booktitle	= {Proceedings of the 12th {ACM} {SIGPLAN} International
		  Conference on Certified Programs and Proofs, {CPP} 2023,
		  Boston, MA, USA, January 16-17, 2023},
  pages		= {253--266},
  publisher	= {{ACM}},
  year		= {2023},
  url		= {https://doi.org/10.1145/3573105.3575671},
  doi		= {10.1145/3573105.3575671},
  timestamp	= {Fri, 13 Jan 2023 13:05:42 +0100},
  biburl	= {https://dblp.org/rec/conf/cpp/LimpergF23.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  Livingston23,
  author	= {Livingston, Amelia},
  title		= {{Group Cohomology in the Lean Community Library}},
  booktitle	= {14th International Conference on Interactive Theorem
		  Proving (ITP 2023)},
  pages		= {22:1--22:17},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-284-6},
  issn		= {1868-8969},
  year		= {2023},
  volume	= {268},
  editor	= {Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/opus/volltexte/2023/18397},
  urn		= {urn:nbn:de:0030-drops-183974},
  doi		= {10.4230/LIPIcs.ITP.2023.22},
  annote	= {Keywords: formal math, Lean, mathlib, group cohomology,
		  homological algebra}
}

@Article{	  LS25,
  title		= {Formalizing zeta and {L}-functions in Lean},
  author	= {David Loeffler and Michael Stoll},
  url		= {https://afm.episciences.org/15328},
  doi		= {10.46298/afm.15328},
  journal	= {Annals of Formalized Mathematics},
  volume	= {Volume 1},
  eid		= 2,
  year		= {2025},
  month		= {Jul},
  keywords	= {Number Theory, Formal Languages and Automata Theory, Logic
		  in Computer Science}
}

@Article{	  Madelaine19,
  author	= {Paul{-}Nicolas Madelaine},
  title		= {Arithmetic and Casting in Lean},
  url		= {https://lean-forward.github.io/norm_cast/norm_cast.pdf},
  year		= {2019}
}

@InProceedings{	  Massot24,
  author	= {Massot, Patrick},
  title		= {{Teaching Mathematics Using Lean and Controlled Natural
		  Language}},
  booktitle	= {15th International Conference on Interactive Theorem
		  Proving (ITP 2024)},
  pages		= {27:1--27:19},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-337-9},
  issn		= {1868-8969},
  year		= {2024},
  volume	= {309},
  editor	= {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.27},
  urn		= {urn:nbn:de:0030-drops-207550},
  doi		= {10.4230/LIPIcs.ITP.2024.27},
  annote	= {Keywords: mathematics teaching, proof assistant,
		  controlled natural language}
}

@InProceedings{	  Mathlib,
  title		= {The {L}ean mathematical library},
  booktitle	= {Proceedings of the 9th {ACM} {SIGPLAN} International
		  Conference on Certified Programs and Proofs, {CPP} 2020,
		  New Orleans, LA, USA, January 20-21, 2020},
  author	= {{The mathlib community}},
  pages		= {367--381},
  year		= {2020},
  url		= {https://doi.org/10.1145/3372885.3373824},
  doi		= {10.1145/3372885.3373824},
  timestamp	= {Thu, 23 Jan 2020 16:12:31 +0100},
  biburl	= {https://dblp.org/rec/conf/cpp/X20.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  Mehta22,
  author	= {Bhavik Mehta},
  editor	= {Kevin Buzzard and Temur Kutsia},
  title		= {Formalising the Kruskal-Katona Theorem in Lean},
  booktitle	= {Intelligent Computer Mathematics - 15th International
		  Conference, {CICM} 2022, Tbilisi, Georgia, September 19-23,
		  2022, Proceedings},
  series	= {Lecture Notes in Computer Science},
  volume	= {13467},
  pages		= {75--91},
  publisher	= {Springer},
  year		= {2022},
  url		= {https://doi.org/10.1007/978-3-031-16681-5\_5},
  doi		= {10.1007/978-3-031-16681-5\_5},
  timestamp	= {Mon, 19 Sep 2022 18:41:39 +0200},
  biburl	= {https://dblp.org/rec/conf/mkm/Mehta22.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  Mehta23,
  author	= {Bhavik Mehta},
  editor	= {Robbert Krebbers and Dmitriy Traytel and Brigitte Pientka
		  and Steve Zdancewic},
  title		= {Formalising Sharkovsky's Theorem (Proof Pearl)},
  booktitle	= {Proceedings of the 12th {ACM} {SIGPLAN} International
		  Conference on Certified Programs and Proofs, {CPP} 2023,
		  Boston, MA, USA, January 16-17, 2023},
  pages		= {267--274},
  publisher	= {{ACM}},
  year		= {2023},
  url		= {https://doi.org/10.1145/3573105.3575689},
  doi		= {10.1145/3573105.3575689},
  timestamp	= {Fri, 13 Jan 2023 13:05:42 +0100},
  biburl	= {https://dblp.org/rec/conf/cpp/Mehta23.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Article{	  Merc25,
  title		= {Formalising the local compactness of the adele ring},
  author	= {Salvatore Mercuri},
  url		= {https://afm.episciences.org/14840},
  doi		= {10.46298/afm.14840},
  journal	= {Annals of Formalized Mathematics},
  volume	= {Volume 1},
  eid		= 5,
  year		= {2025},
  month		= {Jul},
  keywords	= {Logic in Computer Science, Number Theory}
}

@InProceedings{	  Nash23,
  author	= {Nash, Oliver},
  title		= {{A Formalisation of Gallagher’s Ergodic Theorem}},
  booktitle	= {14th International Conference on Interactive Theorem
		  Proving (ITP 2023)},
  pages		= {23:1--23:16},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-284-6},
  issn		= {1868-8969},
  year		= {2023},
  volume	= {268},
  editor	= {Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/opus/volltexte/2023/18398},
  urn		= {urn:nbn:de:0030-drops-183981},
  doi		= {10.4230/LIPIcs.ITP.2023.23},
  annote	= {Keywords: Lean proof assistant, measure theory, metric
		  number theory, ergodicity, Gallagher’s theorem,
		  Duffin-Schaeffer conjecture}
}

@InProceedings{	  NawrockiAyersEbner23,
  author	= {Nawrocki, Wojciech and Ayers, Edward W. and Ebner,
		  Gabriel},
  title		= {{An Extensible User Interface for Lean 4}},
  booktitle	= {14th International Conference on Interactive Theorem
		  Proving (ITP 2023)},
  pages		= {24:1--24:20},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-284-6},
  issn		= {1868-8969},
  year		= {2023},
  volume	= {268},
  editor	= {Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/opus/volltexte/2023/18399},
  urn		= {urn:nbn:de:0030-drops-183991},
  doi		= {10.4230/LIPIcs.ITP.2023.24},
  annote	= {Keywords: user interfaces, human-computer interaction,
		  Lean}
}

@InProceedings{	  norman_et_al:LIPIcs.ITP.2025.14,
  author	= {Norman, Chase and Avigad, Jeremy},
  title		= {{Canonical for Automated Theorem Proving in Lean}},
  booktitle	= {16th International Conference on Interactive Theorem
		  Proving (ITP 2025)},
  year		= {2025},
  editor	= {Forster, Yannick and Keller, Chantal},
  volume	= {352},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  pages		= {14:1--14:20},
  address	= {Dagstuhl, Germany},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  annote	= {Keywords: Automated Reasoning, Interactive Theorem
		  Proving, Dependent Type Theory, Inhabitation, Unification,
		  Program Synthesis, Formal Methods},
  doi		= {10.4230/LIPIcs.ITP.2025.14},
  isbn		= {978-3-95977-396-6},
  issn		= {1868-8969},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.14},
  urn		= {urn:nbn:de:0030-drops-246128}
}

@InProceedings{	  ObendraufBaanenKoopmanStebletsova24,
  author	= {Obendrauf, Kai and Baanen, Anne and Koopmann, Patrick and
		  Stebletsova, Vera},
  title		= {{Lean Formalization of Completeness Proof for Coalition
		  Logic with Common Knowledge}},
  booktitle	= {15th International Conference on Interactive Theorem
		  Proving (ITP 2024)},
  pages		= {28:1--28:18},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-337-9},
  issn		= {1868-8969},
  year		= {2024},
  volume	= {309},
  editor	= {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.28},
  urn		= {urn:nbn:de:0030-drops-207560},
  doi		= {10.4230/LIPIcs.ITP.2024.28},
  annote	= {Keywords: Multi-agent systems, Coalition Logic, Epistemic
		  Logic, common knowledge, completeness, formal methods, Lean
		  prover}
}

@Article{	  PNWT22,
  author	= {Porncharoenwase, Sorawee and Nelson, Luke and Wang, Xi and
		  Torlak, Emina},
  title		= {A Formal Foundation for Symbolic Evaluation with Merging},
  year		= {2022},
  issue_date	= {January 2022},
  publisher	= {Association for Computing Machinery},
  address	= {New York, NY, USA},
  volume	= {6},
  number	= {POPL},
  url		= {https://doi.org/10.1145/3498709},
  doi		= {10.1145/3498709},
  abstract	= {Reusable symbolic evaluators are a key building block of
		  solver-aided verification and synthesis tools. A reusable
		  evaluator reduces the semantics of all paths in a program
		  to logical constraints, and a client tool uses these
		  constraints to formulate a satisfiability query that is
		  discharged with SAT or SMT solvers. The correctness of the
		  evaluator is critical to the soundness of the tool and the
		  domain properties it aims to guarantee. Yet so far, the
		  trust in these evaluators has been based on an ad-hoc
		  foundation of testing and manual reasoning. This paper
		  presents the first formal framework for reasoning about the
		  behavior of reusable symbolic evaluators. We develop a new
		  symbolic semantics for these evaluators that incorporates
		  state merging. Symbolic evaluators use state merging to
		  avoid path explosion and generate compact encodings. To
		  accommodate a wide range of implementations, our semantics
		  is parameterized by a symbolic factory, which abstracts
		  away the details of merging and creation of symbolic
		  values. The semantics targets a rich language that extends
		  Core Scheme with assumptions and assertions, and thus
		  supports branching, loops, and (first-class) procedures.
		  The semantics is designed to support reusability, by
		  guaranteeing two key properties: legality of the generated
		  symbolic states, and the reducibility of symbolic
		  evaluation to concrete evaluation. Legality makes it
		  simpler for client tools to formulate queries, and
		  reducibility enables testing of client tools on concrete
		  inputs. We use the Lean theorem prover to mechanize our
		  symbolic semantics, prove that it is sound and complete
		  with respect to the concrete semantics, and prove that it
		  guarantees legality and reducibility. To demonstrate the
		  generality of our semantics, we develop Leanette, a
		  reference evaluator written in Lean, and Rosette 4, an
		  optimized evaluator written in Racket. We prove Leanette
		  correct with respect to the semantics, and validate Rosette
		  4 against Leanette via solver-aided differential testing.
		  To demonstrate the practicality of our approach, we port 16
		  published verification and synthesis tools from Rosette 3
		  to Rosette 4. Rosette 3 is an existing reusable evaluator
		  that implements the classic merging semantics, adopted from
		  bounded model checking. Rosette 4 replaces the semantic
		  core of Rosette 3 but keeps its optimized symbolic factory.
		  Our results show that Rosette 4 matches the performance of
		  Rosette 3 across a wide range of benchmarks, while
		  providing a cleaner interface that simplifies the
		  implementation of client tools.},
  journal	= {Proc. ACM Program. Lang.},
  month		= jan,
  articleno	= {47},
  numpages	= {28},
  keywords	= {state merging, symbolic evaluation}
}

@Article{	  PorncharoenwasePombrioTorlak2023,
  author	= {Porncharoenwase, Sorawee and Pombrio, Justin and Torlak,
		  Emina},
  title		= {A Pretty Expressive Printer},
  year		= {2023},
  issue_date	= {October 2023},
  publisher	= {Association for Computing Machinery},
  address	= {New York, NY, USA},
  volume	= {7},
  number	= {OOPSLA2},
  url		= {https://doi.org/10.1145/3622837},
  doi		= {10.1145/3622837},
  abstract	= {Pretty printers make trade-offs between the expressiveness
		  of their pretty printing language, the optimality objective
		  that they minimize when choosing between different ways to
		  lay out a document, and the performance of their algorithm.
		  This paper presents a new pretty printer, Πe, that is
		  strictly more expressive than all pretty printers in the
		  literature and provably minimizes an optimality objective.
		  Furthermore, the time complexity of Πe is better than many
		  existing pretty printers. When choosing among different
		  ways to lay out a document, Πe consults a user-supplied
		  cost factory, which determines the optimality objective,
		  giving Πe a unique degree of flexibility. We use the Lean
		  theorem prover to verify the correctness (validity and
		  optimality) of Πe, and implement Πe concretely as a
		  pretty printer that we call PrettyExpressive. To evaluate
		  our pretty printer against others, we develop a formal
		  framework for reasoning about the expressiveness of pretty
		  printing languages, and survey pretty printers in the
		  literature, comparing their expressiveness, optimality,
		  worst-case time complexity, and practical running time. Our
		  evaluation shows that PrettyExpressive is efficient and
		  effective at producing optimal layouts. PrettyExpressive
		  has also seen real-world adoption: it serves as a
		  foundation of a code formatter for Racket.},
  journal	= {Proc. ACM Program. Lang.},
  month		= oct,
  articleno	= {261},
  numpages	= {28},
  keywords	= {pretty printing}
}

@Article{	  Riou25,
  title		= {Formalization of derived categories in {L}ean/mathlib},
  author	= {Joël Riou},
  url		= {https://afm.episciences.org/13609},
  doi		= {10.46298/afm.13609},
  journal	= {Annals of Formalized Mathematics},
  volume	= {Volume 1},
  eid		= 1,
  year		= {2025},
  month		= {Jul},
  keywords	= {Derived category, Homological algebra, Spectral sequence,
		  MSC 2020: 18G80, 18G15, 18G40, 18E35, 68V20,
		  [MATH.MATH-CT]Mathematics [math]/Category Theory [math.CT],
		  [INFO.INFO-LO]Computer Science [cs]/Logic in Computer
		  Science [cs.LO]},
  language	= {English}
}

@Article{	  SelsamDeMoura16,
  author	= {Daniel Selsam and Leonardo {de Moura}},
  title		= {Congruence Closure in Intensional Type Theory},
  booktitle	= {Automated Reasoning - 8th International Joint Conference,
		  {IJCAR} 2016, Coimbra, Portugal, June 27 - July 2, 2016,
		  Proceedings},
  pages		= {99--115},
  year		= {2016},
  crossref	= {DBLP:conf/cade/2016},
  url		= "\url{https://doi.org/10.1007/978-3-319-40229-1_8}",
  doi		= {10.1007/978-3-319-40229-1\_8},
  timestamp	= {Wed, 06 Nov 2019 16:45:49 +0100},
  biburl	= {https://dblp.org/rec/conf/cade/SelsamM16.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Article{	  SelsamHudonDeMoura20,
  author	= {Selsam, Daniel and Hudon, Simon and {de Moura}, Leonardo},
  title		= {Sealing Pointer-Based Optimizations behind Pure
		  Functions},
  year		= {2020},
  issue_date	= {August 2020},
  publisher	= {Association for Computing Machinery},
  address	= {New York, NY, USA},
  volume	= {4},
  number	= {ICFP},
  url		= {https://doi.org/10.1145/3408997},
  doi		= {10.1145/3408997},
  abstract	= {Functional programming languages are particularly
		  well-suited for building automated reasoning systems, since
		  (among other reasons) a logical term is well modeled by an
		  inductive type, traversing a term can be implemented
		  generically as a higher-order combinator, and backtracking
		  search is dramatically simplified by persistent
		  datastructures. However, existing pure functional
		  programming languages all suffer a major limitation in
		  these domains: traversing a term requires time proportional
		  to the tree size of the term as opposed to its graph size.
		  This limitation would be particularly devastating when
		  building automation for interactive theorem provers such as
		  Lean and Coq, for which the exponential blowup of term-tree
		  sizes has proved to be both common and difficult to
		  prevent. All that is needed to recover the optimal scaling
		  is the ability to perform simple operations on the memory
		  addresses of terms, and yet allowing these operations to be
		  used freely would clearly violate the basic premise of
		  referential transparency. We show how to use dependent
		  types to seal the necessary pointer-address manipulations
		  behind pure functional interfaces while requiring only a
		  negligible amount of additional trust. We have implemented
		  our approach for the upcoming version (v4) of Lean, and our
		  approach could be adopted by other languages based on
		  dependent type theory as well.},
  journal	= {Proc. ACM Program. Lang.},
  month		= aug,
  articleno	= {115},
  numpages	= {20},
  keywords	= {interactive theorem proving, Lean, functional
		  programming}
}

@InProceedings{	  SelsamLD17,
  author	= {Daniel Selsam and Percy Liang and David L. Dill},
  title		= {Developing Bug-Free Machine Learning Systems With Formal
		  Mathematics},
  booktitle	= {Proceedings of the 34th International Conference on
		  Machine Learning, {ICML} 2017, Sydney, NSW, Australia, 6-11
		  August 2017},
  pages		= {3047--3056},
  year		= {2017},
  crossref	= {DBLP:conf/icml/2017},
  url		= {http://proceedings.mlr.press/v70/selsam17a.html},
  timestamp	= {Wed, 29 May 2019 08:41:45 +0200},
  biburl	= {https://dblp.org/rec/bib/conf/icml/SelsamLD17},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Misc{		  SelsamUllrichDeMoura20,
  author	= {Daniel Selsam and Sebastian Ullrich and Leonardo {de
		  Moura}},
  title		= {Tabled Typeclass Resolution},
  journal	= {CoRR},
  volume	= {abs/2001.04301},
  year		= {2020},
  url		= {https://arxiv.org/abs/2001.04301},
  archiveprefix	= {arXiv},
  eprint	= {2001.04301},
  timestamp	= {Fri, 17 Jan 2020 14:07:30 +0100},
  biburl	= {https://dblp.org/rec/journals/corr/abs-2001-04301.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Misc{		  StricklandBellumat19,
  author	= {Neil Strickland and Nicola Bellumat},
  title		= {Iterated chromatic localisation},
  year		= {2019},
  eprint	= {arXiv:1907.07801}
}

@InProceedings{	  SubercaseauxNawrockiGallicchioCodelCarneiroHeule24,
  author	= {Subercaseaux, Bernardo and Nawrocki, Wojciech and
		  Gallicchio, James and Codel, Cayden and Carneiro, Mario and
		  Heule, Marijn J. H.},
  title		= {{Formal Verification of the Empty Hexagon Number}},
  booktitle	= {15th International Conference on Interactive Theorem
		  Proving (ITP 2024)},
  pages		= {35:1--35:19},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-337-9},
  issn		= {1868-8969},
  year		= {2024},
  volume	= {309},
  editor	= {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.35},
  urn		= {urn:nbn:de:0030-drops-207633},
  doi		= {10.4230/LIPIcs.ITP.2024.35},
  annote	= {Keywords: Empty Hexagon Number, Discrete Computational
		  Geometry, Erd\H{o}s-Szekeres}
}

@InProceedings{	  tantow_et_al:LIPIcs.ITP.2025.36,
  author	= {Tantow, Johannes and Gerlach, Lukas and Mennicke, Stephan
		  and Kr\"{o}tzsch, Markus},
  title		= {{Verifying Datalog Reasoning with Lean}},
  booktitle	= {16th International Conference on Interactive Theorem
		  Proving (ITP 2025)},
  year		= {2025},
  editor	= {Forster, Yannick and Keller, Chantal},
  volume	= {352},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  pages		= {36:1--36:19},
  address	= {Dagstuhl, Germany},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  annote	= {Keywords: Certifying Algorithms, Datalog, Formal
		  Verification},
  doi		= {10.4230/LIPIcs.ITP.2025.36},
  isbn		= {978-3-95977-396-6},
  issn		= {1868-8969},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.36},
  urn		= {urn:nbn:de:0030-drops-246342}
}

@InProceedings{	  TassarottiVBT21,
  author	= {Tassarotti, Joseph and Vajjha, Koundinya and Banerjee,
		  Anindya and Tristan, Jean-Baptiste},
  title		= {A Formal Proof of PAC Learnability for Decision Stumps},
  year		= {2021},
  isbn		= {9781450382991},
  publisher	= {Association for Computing Machinery},
  address	= {New York, NY, USA},
  url		= {https://doi.org/10.1145/3437992.3439917},
  doi		= {10.1145/3437992.3439917},
  abstract	= {We present a formal proof in Lean of probably
		  approximately correct (PAC) learnability of the concept
		  class of decision stumps. This classic result in machine
		  learning theory derives a bound on error probabilities for
		  a simple type of classifier. Though such a proof appears
		  simple on paper, analytic and measure-theoretic subtleties
		  arise when carrying it out fully formally. Our proof is
		  structured so as to separate reasoning about deterministic
		  properties of a learning function from proofs of
		  measurability and analysis of probabilities.},
  booktitle	= {Proceedings of the 10th ACM SIGPLAN International
		  Conference on Certified Programs and Proofs},
  pages		= {5–17},
  numpages	= {13},
  keywords	= {probably approximately correct, interactive theorem
		  proving, decision stumps},
  location	= {Virtual, Denmark},
  series	= {CPP 2021}
}

@Misc{		  Ullrich16,
  author	= {Sebastian Ullrich},
  title		= {Simple Verification of {R}ust Programs via Functional
		  Purification},
  eprint	= {https://github.com/Kha/masters-thesis/blob/master/main.pdf},
  note		= {Masters thesis},
  year		= {2016}
}

@Article{	  UllrichDeMoura19,
  author	= {Sebastian Ullrich and Leonardo {de Moura}},
  title		= {Counting Immutable Beans: Reference Counting Optimized for
		  Purely Functional Programming},
  year		= {2019},
  url		= {http://arxiv.org/abs/1908.05647},
  archiveprefix	= {arXiv},
  eprint	= {1908.05647}
}

@InProceedings{	  UllrichDeMoura20,
  author	= {Sebastian Ullrich and Leonardo {de Moura}},
  editor	= {Nicolas Peltier and Viorica Sofronie{-}Stokkermans},
  title		= {Beyond Notations: Hygienic Macro Expansion for Theorem
		  Proving Languages},
  booktitle	= {Automated Reasoning - 10th International Joint Conference,
		  {IJCAR} 2020, Paris, France, July 1-4, 2020, Proceedings,
		  Part {II}},
  series	= {Lecture Notes in Computer Science},
  volume	= {12167},
  pages		= {167--182},
  publisher	= {Springer},
  year		= {2020},
  url		= {https://doi.org/10.1007/978-3-030-51054-1\_10},
  doi		= {10.1007/978-3-030-51054-1\_10},
  timestamp	= {Fri, 03 Jul 2020 14:00:29 +0200},
  biburl	= {https://dblp.org/rec/conf/cade/0002M20.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Article{	  UllrichDeMoura22,
  author	= {Sebastian Ullrich and Leonardo de Moura},
  title		= {'do' unchained: embracing local imperativity in a purely
		  functional language (functional pearl)},
  journal	= {Proc. {ACM} Program. Lang.},
  volume	= {6},
  number	= {{ICFP}},
  pages		= {512--539},
  year		= {2022},
  url		= {https://doi.org/10.1145/3547640},
  doi		= {10.1145/3547640},
  timestamp	= {Tue, 18 Oct 2022 22:18:46 +0200},
  biburl	= {https://dblp.org/rec/journals/pacmpl/UllrichM22.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  VanDoornEbnerLewis20,
  author	= {Floris {van Doorn} and Gabriel Ebner and Robert Y. Lewis},
  title		= {Maintaining a Library of Formal Mathematics},
  booktitle	= {Intelligent Computer Mathematics, CICM 2020},
  volume	= {abs/2004.03673},
  year		= {2020},
  url		= {https://arxiv.org/abs/2004.03673},
  archiveprefix	= {arXiv},
  eprint	= {2004.03673},
  timestamp	= {Tue, 14 Apr 2020 16:40:34 +0200},
  biburl	= {https://dblp.org/rec/journals/corr/abs-2004-03673.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  vanDoornMacbeth24,
  author	= {van Doorn, Floris and Macbeth, Heather},
  title		= {{Integrals Within Integrals: A Formalization of the
		  Gagliardo-Nirenberg-Sobolev Inequality}},
  booktitle	= {15th International Conference on Interactive Theorem
		  Proving (ITP 2024)},
  pages		= {37:1--37:18},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-337-9},
  issn		= {1868-8969},
  year		= {2024},
  volume	= {309},
  editor	= {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.37},
  urn		= {urn:nbn:de:0030-drops-207657},
  doi		= {10.4230/LIPIcs.ITP.2024.37},
  annote	= {Keywords: Sobolev inequality, measure theory, Lean,
		  formalized mathematics}
}

@InProceedings{	  vin_et_al:LIPIcs.ITP.2025.37,
  author	= {Vin, Eric and Miller, Kyle A. and Fremont, Daniel J.},
  title		= {{LeanLTL: A Unifying Framework for Linear Temporal Logics
		  in Lean}},
  booktitle	= {16th International Conference on Interactive Theorem
		  Proving (ITP 2025)},
  year		= {2025},
  editor	= {Forster, Yannick and Keller, Chantal},
  volume	= {352},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  pages		= {37:1--37:9},
  address	= {Dagstuhl, Germany},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  annote	= {Keywords: Linear Temporal Logic, Interactive Theorem
		  Proving, Lean 4},
  doi		= {10.4230/LIPIcs.ITP.2025.37},
  isbn		= {978-3-95977-396-6},
  issn		= {1868-8969},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.37},
  urn		= {urn:nbn:de:0030-drops-246356}
}

@Misc{		  VonRaumer15,
  author	= {Jakob {von Raumer}},
  title		= {Formalization of Non-Abelian Topology for Homotopy Type
		  Theory},
  eprint	= {http://www.contrib.andrew.cmu.edu/~avigad/Students/von_raumer_thesis.pdf},
  note		= {Masters thesis},
  year		= {2015}
}

@InProceedings{	  VonRaumer16,
  author	= {Jakob {von Raumer}},
  title		= {Formalizing Double Groupoids and Cross Modules in the Lean
		  Theorem Prover},
  booktitle	= {Mathematical Software - {ICMS} 2016 - 5th International
		  Conference, Berlin, Germany, July 11-14, 2016,
		  Proceedings},
  pages		= {28--33},
  year		= {2016},
  crossref	= {DBLP:conf/icms/2016},
  url		= "\url{https://doi.org/10.1007/978-3-319-42432-3_4}",
  doi		= {10.1007/978-3-319-42432-3\_4},
  timestamp	= {Tue, 14 May 2019 10:00:40 +0200},
  biburl	= {https://dblp.org/rec/bib/conf/icms/Raumer16},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  wang_et_al:LIPIcs.ITP.2025.9,
  author	= {Wang, Eric and Bhoja, Arohee and Codel, Cayden and Singer,
		  Noah G.},
  title		= {{Algebra Is Half the Battle: Verifying Presentations of
		  Graded Unipotent Chevalley Groups}},
  booktitle	= {16th International Conference on Interactive Theorem
		  Proving (ITP 2025)},
  year		= {2025},
  editor	= {Forster, Yannick and Keller, Chantal},
  volume	= {352},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  pages		= {9:1--9:19},
  address	= {Dagstuhl, Germany},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  annote	= {Keywords: Group presentations, term rewriting,
		  metaprogramming, proof automation, the Lean theorem
		  prover},
  doi		= {10.4230/LIPIcs.ITP.2025.9},
  isbn		= {978-3-95977-396-6},
  issn		= {1868-8969},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.9},
  urn		= {urn:nbn:de:0030-drops-246071}
}

@Article{	  Wieser2021,
  author	= {Eric Wieser},
  title		= {Scalar actions in Lean's mathlib},
  journal	= {CoRR},
  volume	= {abs/2108.10700},
  year		= {2021},
  url		= {https://arxiv.org/abs/2108.10700},
  eprinttype	= {arXiv},
  eprint	= {2108.10700},
  timestamp	= {Fri, 27 Aug 2021 15:02:29 +0200},
  biburl	= {https://dblp.org/rec/journals/corr/abs-2108-10700.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Article{	  Wieser2022,
  author	= {Eric Wieser and Utensil Song},
  title		= {Formalizing Geometric Algebra in Lean},
  journal	= {Advances in Applied Clifford Algebras},
  publisher	= {Springer},
  volume	= {32},
  number	= {3},
  year		= {2022},
  month		= apr,
  url		= {https://doi.org/10.1007/s00006-021-01164-1},
  doi		= {10.1007/s00006-021-01164-1}
}

@InProceedings{	  WieserCICM23,
  author	= {Eric Wieser},
  editor	= {Catherine Dubois and Manfred Kerber},
  title		= {Multiple-Inheritance Hazards in Dependently-Typed
		  Algebraic Hierarchies},
  booktitle	= {Intelligent Computer Mathematics},
  year		= {2023},
  month		= aug,
  publisher	= {Springer Nature Switzerland},
  address	= {Cham},
  pages		= {222--236},
  isbn		= {978-3-031-42753-4},
  url		= {https://doi.org/10.1007/978-3-031-42753-4_15},
  doi		= {10.1007/978-3-031-42753-4_15}
}

@InProceedings{	  WieserZhang22,
  author	= {Eric Wieser and Jujian Zhang},
  editor	= {Kevin Buzzard and Temur Kutsia},
  title		= {Graded Rings in Lean's Dependent Type Theory},
  booktitle	= {Intelligent Computer Mathematics - 15th International
		  Conference, {CICM} 2022, Tbilisi, Georgia, September 19-23,
		  2022, Proceedings},
  series	= {Lecture Notes in Computer Science},
  volume	= {13467},
  pages		= {122--137},
  publisher	= {Springer},
  year		= {2022},
  url		= {https://doi.org/10.1007/978-3-031-16681-5\_8},
  doi		= {10.1007/978-3-031-16681-5\_8},
  timestamp	= {Mon, 19 Sep 2022 18:41:39 +0200},
  biburl	= {https://dblp.org/rec/conf/mkm/WieserZ22.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  WuGore19,
  author	= {Minchao Wu and Rajeev Gor{\'{e}}},
  title		= {Verified Decision Procedures for Modal Logics},
  booktitle	= {10th International Conference on Interactive Theorem
		  Proving, {ITP} 2019, September 9-12, 2019, Portland, OR,
		  {USA}},
  pages		= {31:1--31:19},
  year		= {2019},
  url		= {https://doi.org/10.4230/LIPIcs.ITP.2019.31},
  doi		= {10.4230/LIPIcs.ITP.2019.31},
  timestamp	= {Mon, 23 Sep 2019 17:27:15 +0200},
  biburl	= {https://dblp.org/rec/conf/itp/WuG19.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  YingDegenne23,
  author	= {Kexing Ying and R{\'{e}}my Degenne},
  editor	= {Robbert Krebbers and Dmitriy Traytel and Brigitte Pientka
		  and Steve Zdancewic},
  title		= {A Formalization of {D}oob's Martingale Convergence
		  Theorems in mathlib},
  booktitle	= {Proceedings of the 12th {ACM} {SIGPLAN} International
		  Conference on Certified Programs and Proofs, {CPP} 2023,
		  Boston, MA, USA, January 16-17, 2023},
  pages		= {334--347},
  publisher	= {{ACM}},
  year		= {2023},
  url		= {https://doi.org/10.1145/3573105.3575675},
  doi		= {10.1145/3573105.3575675},
  timestamp	= {Fri, 13 Jan 2023 13:05:42 +0100},
  biburl	= {https://dblp.org/rec/conf/cpp/YingD23.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  Zhang23,
  author	= {Zhang, Jujian},
  title		= {{Formalising the Proj Construction in Lean}},
  booktitle	= {14th International Conference on Interactive Theorem
		  Proving (ITP 2023)},
  pages		= {35:1--35:17},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-284-6},
  issn		= {1868-8969},
  year		= {2023},
  volume	= {268},
  editor	= {Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.35},
  urn		= {urn:nbn:de:0030-drops-184105},
  doi		= {10.4230/LIPIcs.ITP.2023.35},
  annote	= {Keywords: Lean, formalisation, algebraic geometry, scheme,
		  Proj construction, projective geometry}
}

@InProceedings{	  zhuchko_et_al:LIPIcs.ITP.2025.16,
  author	= {Zhuchko, Ekaterina and Maarand, Hendrik and Veanes, Margus
		  and Ebner, Gabriel},
  title		= {{Finiteness of Symbolic Derivatives in Lean}},
  booktitle	= {16th International Conference on Interactive Theorem
		  Proving (ITP 2025)},
  year		= {2025},
  editor	= {Forster, Yannick and Keller, Chantal},
  volume	= {352},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  pages		= {16:1--16:19},
  address	= {Dagstuhl, Germany},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  annote	= {Keywords: Lean, regular languages, lookarounds,
		  derivatives, finiteness},
  doi		= {10.4230/LIPIcs.ITP.2025.16},
  isbn		= {978-3-95977-396-6},
  issn		= {1868-8969},
  url		= {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.16},
  urn		= {urn:nbn:de:0030-drops-246144}
}