# 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} }