lean.bib

# To normalize:
# bibtool --preserve.key.case=on --preserve.keys=on --pass.comments=on --print.use.tab=off -s -i lean.bib -o lean.bib
@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
                  },
  tags          = {formalization, lean4}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean4}
}

@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},
  website       = {https://github.com/avigad/qpf}
}

@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},
  tags          = {about-mathlib, lean3}
}

@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},
  tags          = {about-mathlib, lean3}
}

@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},
  tags          = {formalization, lean3},
  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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean4}
}

@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},
  tags          = {formalization, lean4}
}

@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},
  tags          = {about-mathlib, lean3}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean4}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  website       = {https://leanprover-community.github.io/lean-perfectoid-spaces/},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  website       = {https://github.com/leanprover-community/mathlib/tree/master/src/computability},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean4}
}

@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.},
  tags          = {about-lean, lean3}
}

@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},
  tags          = {formalization, lean4}
}

@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},
  tags          = {formalization, lean3},
  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},
  tags          = {formalization, lean4}
}

@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},
  website       = {https://leanprover-community.github.io/witt-vectors/},
  tags          = {formalization, lean3}
}

@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},
  website       = {https://github.com/lean-forward/cap_set_problem},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {about-lean, lean2}
}

@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},
  tags          = {about-lean, lean2}
}

@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},
  tags          = {lean4, about-lean}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean2}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean3},
  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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {about-lean, lean3}
}

@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},
  tags          = {formalization, lean4}
}

@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},
  website       = {https://github.com/ramonfmir/lean-scheme},
  tags          = {formalization, lean3}
}

@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},
  tags          = {about-mathlib, lean4}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {about-mathlib, lean4}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  website       = {https://flypitch.github.io/},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  website       = {https://github.com/mhuisi/rc-correctness},
  tags          = {about-lean, lean4}
}

@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]},
  tags          = {formalization, lean3},
  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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  website       = {https://sf.snu.ac.kr/aliveinlean/}
}

@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},
  website       = {https://robertylewis.com/leanmm/},
  tags          = {about-mathlib, lean3}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {about-mathlib, lean3}
}

@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},
  website       = {https://robertylewis.com/leanmm},
  doi           = {https://doi.org/10.1007/s10817-021-09611-1},
  tags          = {about-mathlib, lean3}
}

@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},
  tags          = {about-mathlib, lean3}
}

@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},
  tags          = {about-mathlib, lean4},
  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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean4}
}

@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},
  tags          = {about-mathlib, lean3}
}

@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},
  tags          = {formalization, lean4}
}

@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},
  website       = {https://leanprover-community.github.io/},
  tags          = {about-mathlib, lean3}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean3},
  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},
  tags          = {formalization, lean4}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {about-lean, lean4}
}

@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},
  tags          = {about-mathlib, lean4}
}

@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},
  tags          = {formalization, lean4}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean4}
}

@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},
  tags          = {formalization, lean4}
}

@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},
  tags          = {about-lean, lean2}
}

@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},
  tags          = {about-lean, lean4}
}

@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},
  website       = {https://github.com/dselsam/certigrad}
}

@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},
  tags          = {about-lean, lean4}
}

@Misc{            StricklandBellumat19,
  author        = {Neil Strickland and Nicola Bellumat},
  title         = {Iterated chromatic localisation},
  year          = {2019},
  eprint        = {arXiv:1907.07801},
  website       = {https://github.com/NeilStrickland/itloc},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean4}
}

@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},
  tags          = {formalization, lean4}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  website       = {https://github.com/Kha/electrolysis},
  tags          = {formalization, lean2}
}

@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},
  tags          = {about-lean, lean4}
}

@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},
  tags          = {about-lean, lean4}
}

@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},
  tags          = {about-lean, lean4}
}

@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},
  tags          = {about-mathlib, lean3}
}

@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},
  tags          = {formalization, lean4}
}

@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},
  tags          = {formalization, lean4}
}

@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},
  website       = {https://github.com/javra/msc-thesis},
  tags          = {formalization, lean2}
}

@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},
  tags          = {formalization, lean2}
}

@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},
  tags          = {formalization, lean4}
}

@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},
  tags          = {about-mathlib, lean3}
}

@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},
  tags          = {formalization, lean3},
  website       = {https://github.com/pygae/lean-ga}
}

@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},
  tags          = {formalization, lean3, lean4}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  website       = {https://github.com/minchaowu/ModalTab}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean3}
}

@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},
  tags          = {formalization, lean4}
}