diff --git a/lean.bib b/lean.bib index 54397077f..16e3c33da 100644 --- a/lean.bib +++ b/lean.bib @@ -1,6 +1,4 @@ -# 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}, @@ -13,8 +11,7 @@ @Article{ ABKNT_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, @@ -37,8 +34,7 @@ @InProceedings{ AGLST23 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} + interactive proof systems} } @InProceedings{ AngdinataXu23, @@ -61,12 +57,9 @@ @InProceedings{ AngdinataXu23 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} + group law, Lean, mathlib} } -# To normalize: -# bibtool --preserve.key.case=on --preserve.keys=on --pass.comments=on --print.use.tab=off -s -i lean.bib -o lean.bib @InProceedings{ Asgeirsson24, author = {Asgeirsson, Dagur}, title = {{Towards Solid Abelian Groups: A Formal Proof of @@ -87,8 +80,7 @@ @InProceedings{ Asgeirsson24 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} + Lean, Mathlib, Interactive theorem proving} } @Book{ Avig14, @@ -120,8 +112,7 @@ @InProceedings{ AvigadCarneiroHudon19 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{ Baanen20, @@ -141,8 +132,7 @@ @InProceedings{ Baanen20 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{ Baanen22, @@ -165,8 +155,7 @@ @InProceedings{ Baanen22 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} + theory, typeclasses, algebraic hierarchy, Lean prover} } @InProceedings{ BaanenBCD23, @@ -184,7 +173,6 @@ @InProceedings{ BaanenBCD23 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} @@ -211,8 +199,7 @@ @InProceedings{ BaanenDahmenNarayananNuccio21 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} + commutative algebra, Lean, mathlib} } @Article{ BaanenDahmenNarayananNuccio22, @@ -230,8 +217,7 @@ @Article{ BaanenDahmenNarayananNuccio22 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} + url = {https://doi.org/10.1007/s10817-022-09644-0} } @InProceedings{ BasoldBruinLawson24, @@ -253,8 +239,28 @@ @InProceedings{ BasoldBruinLawson24 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} + Directed Homotopy Theory, Formalised Mathematics} +} + +@Article{ BBRBvY25, + title = {A complete formalization of Fermat's Last Theorem for + regular primes in Lean}, + author = {Riccardo Brasca and Christopher Birkbeck and Eric + Rodriguez Boidi and Alex Best and Ruben van De Velde and + Andrew Yang}, + url = {https://afm.episciences.org/14586}, + doi = {10.46298/afm.14586}, + journal = {Annals of Formalized Mathematics}, + volume = {Volume 1}, + eid = 4, + year = {2025}, + month = {Jul}, + keywords = {Lean, Mathlib, Kummer's lemma, [MATH.MATH-NT]Mathematics + [math]/Number Theory [math.NT], [INFO.INFO-LO]Computer + Science [cs]/Logic in Computer Science [cs.LO], + [INFO.INFO-FL]Computer Science [cs]/Formal Languages and + Automata Theory [cs.FL]}, + language = {English} } @Booklet{ Best2021, @@ -262,8 +268,7 @@ @Booklet{ Best2021 title = {Automatically Generalizing Theorems Using Typeclasses}, howpublished = {EasyChair Preprint no. 6216}, url = {https://easychair.org/publications/preprint/KLfT}, - year = {2021}, - tags = {about-mathlib, lean3} + year = {2021} } @InProceedings{ BestBirkbeckBrascaRodriguez23, @@ -286,8 +291,7 @@ @InProceedings{ BestBirkbeckBrascaRodriguez23 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} + Interactive theorem proving, Lean} } @InProceedings{ BhatKeizerHughesGoensGrosser24, @@ -310,8 +314,7 @@ @InProceedings{ BhatKeizerHughesGoensGrosser24 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} + regions, peephole rewrites} } @Article{ BordgCavalleri2021, @@ -326,8 +329,7 @@ @Article{ BordgCavalleri2021 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @Article{ BrowningLutz22, @@ -341,10 +343,10 @@ @Article{ BrowningLutz22 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} + eprint = {https://doi.org/10.1080/10586458.2021.1986176} } +% Encoding: UTF-8 @InProceedings{ Buch18, author = {Ulrik Buchholtz and Floris {van Doorn} and Egbert Rijke}, title = {Higher Groups in Homotopy Type Theory}, @@ -370,9 +372,7 @@ @InProceedings{ BuzzardCommelinMassot20 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @Article{ BuzzardHLLFM21, @@ -389,8 +389,7 @@ @Article{ BuzzardHLLFM21 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{ Carneiro19, @@ -406,9 +405,29 @@ @InProceedings{ Carneiro19 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} + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@InProceedings{ carneiro_et_al:LIPIcs.ITP.2025.20, + author = {Carneiro, Mario and Riehl, Emily}, + title = {{Formalizing Colimits in 𝒞at}}, + booktitle = {16th International Conference on Interactive Theorem + Proving (ITP 2025)}, + year = {2025}, + editor = {Forster, Yannick and Keller, Chantal}, + volume = {352}, + series = {Leibniz International Proceedings in Informatics + (LIPIcs)}, + pages = {20:1--20:19}, + address = {Dagstuhl, Germany}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + annote = {Keywords: category theory, infinity-category theory, + nerve, simplicial set, colimit}, + doi = {10.4230/LIPIcs.ITP.2025.20}, + isbn = {978-3-95977-396-6}, + issn = {1868-8969}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.20}, + urn = {urn:nbn:de:0030-drops-246186} } @Misc{ CarneiroMaster, @@ -418,8 +437,30 @@ @Misc{ CarneiroMaster note = {Master thesis}, year = {2019}, abstract = {Meta-theoretic properties of Lean 3, including - soundness.}, - tags = {about-lean, lean3} + soundness.} +} + +@InProceedings{ chambertloir_et_al:LIPIcs.ITP.2025.4, + author = {Chambert-Loir, Antoine and de Frutos-Fern\'{a}ndez, + Mar{\'\i}a In\'{e}s}, + title = {{A Formalization of Divided Powers in Lean}}, + booktitle = {16th International Conference on Interactive Theorem + Proving (ITP 2025)}, + year = {2025}, + editor = {Forster, Yannick and Keller, Chantal}, + volume = {352}, + series = {Leibniz International Proceedings in Informatics + (LIPIcs)}, + pages = {4:1--4:17}, + address = {Dagstuhl, Germany}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + annote = {Keywords: Formal mathematics, algebraic number theory, + commutative algebra, divided powers, Lean, Mathlib}, + doi = {10.4230/LIPIcs.ITP.2025.4}, + isbn = {978-3-95977-396-6}, + issn = {1868-8969}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.4}, + urn = {urn:nbn:de:0030-drops-246038} } @InProceedings{ Clune23, @@ -435,7 +476,6 @@ @InProceedings{ Clune23 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} @@ -462,8 +502,7 @@ @InProceedings{ CluneQianBentkampAvigad24 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} + interactive theorem proving, Lean, dependent type theory} } @InProceedings{ CommelinLewis21, @@ -502,9 +541,7 @@ @InProceedings{ CommelinLewis21 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} + series = {CPP 2021} } @InProceedings{ DahmenHolzlLewis19, @@ -520,9 +557,7 @@ @InProceedings{ DahmenHolzlLewis19 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{ deFrutos22, @@ -544,8 +579,7 @@ @InProceedings{ deFrutos22 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} + field theory, Lean, mathlib} } @InProceedings{ deFrutos23, @@ -569,8 +603,7 @@ @InProceedings{ deFrutos23 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} + p-adic Hodge theory} } @InProceedings{ deFrutosNuccio24, @@ -606,8 +639,7 @@ @InProceedings{ deFrutosNuccio24 numpages = {15}, keywords = {mathlib, local fields, formal mathematics, discrete valuation rings, algebraic number theory, Lean}, - series = {CPP 2024}, - tags = {formalization, lean3} + series = {CPP 2024} } @Misc{ DeMoura15, @@ -616,8 +648,7 @@ @Misc{ DeMoura15 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} + abstract = {Elaboration in Lean 2} } @InProceedings{ DeMouraKongAvigadVanDoornvonRaumer, @@ -635,8 +666,7 @@ @InProceedings{ DeMouraKongAvigadVanDoornvonRaumer 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} + abstract = {System description of Lean 2} } @InProceedings{ deMouraUllrich2021, @@ -664,8 +694,7 @@ @InProceedings{ deMouraUllrich2021 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} + url = {https://link.springer.com/chapter/10.1007/978-3-030-79876-5_37} } @InProceedings{ DilliesMehta22, @@ -688,8 +717,7 @@ @InProceedings{ DilliesMehta22 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} + Regularity Lemma, Roth’s Theorem} } @InProceedings{ Door16, @@ -706,8 +734,7 @@ @InProceedings{ Door16 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{ Door17, @@ -746,8 +773,7 @@ @InProceedings{ Door21 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} + Lean, interactive theorem proving, formalized mathematics} } @InProceedings{ DoornMN23, @@ -763,7 +789,6 @@ @InProceedings{ DoornMN23 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} @@ -789,8 +814,7 @@ @Article{ DupuisLewisMacbeth22 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} + semilinear, Hilbert space} } @InProceedings{ dvorak_et_al:LIPIcs.ITP.2023.15, @@ -813,8 +837,7 @@ @InProceedings{ dvorak_et_al: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} + languages, Kleene star} } @Article{ EURAM17, @@ -830,8 +853,7 @@ @Article{ EURAM17 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{ Ezeh24, @@ -854,8 +876,7 @@ @InProceedings{ Ezeh24 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} + User Interface} } @Misc{ FernandezMir19, @@ -863,9 +884,31 @@ @Misc{ FernandezMir19 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} + year = {2019} +} + +@InProceedings{ gandhi_et_al:LIPIcs.ITP.2025.12, + author = {Gandhi, Anshula and Tadipatri, Anand Rao and Gowers, + Timothy}, + title = {{Automatically Generalizing Proofs and Statements}}, + booktitle = {16th International Conference on Interactive Theorem + Proving (ITP 2025)}, + year = {2025}, + editor = {Forster, Yannick and Keller, Chantal}, + volume = {352}, + series = {Leibniz International Proceedings in Informatics + (LIPIcs)}, + pages = {12:1--12:18}, + address = {Dagstuhl, Germany}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + annote = {Keywords: automated reasoning, automated theorem proving, + interactive theorem proving, formalization of mathematics, + generalization, Lean theorem prover, Lean tactic}, + doi = {10.4230/LIPIcs.ITP.2025.12}, + isbn = {978-3-95977-396-6}, + issn = {1868-8969}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.12}, + urn = {urn:nbn:de:0030-drops-246104} } @Article{ Gouezel2021, @@ -879,8 +922,7 @@ @Article{ Gouezel2021 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{ Gouezel22, @@ -900,8 +942,7 @@ @InProceedings{ Gouezel22 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @Misc{ GusakovMehtaMiller21, @@ -911,8 +952,7 @@ @Misc{ GusakovMehtaMiller21 eprint = {2101.00127}, archiveprefix = {arXiv}, primaryclass = {math.CO}, - url = {https://arxiv.org/abs/2101.00127}, - tags = {formalization, lean3} + url = {https://arxiv.org/abs/2101.00127} } @InProceedings{ HanVanDoorn, @@ -928,9 +968,7 @@ @InProceedings{ HanVanDoorn 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{ HanVanDoorn19, @@ -947,8 +985,7 @@ @InProceedings{ HanVanDoorn19 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @Misc{ Huisinga19, @@ -957,9 +994,7 @@ @Misc{ Huisinga19 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} + year = {2019} } @InCollection{ KjosHanssenNiraulaYoon22, @@ -971,7 +1006,6 @@ @InCollection{ KjosHanssenNiraulaYoon22 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} } @@ -981,8 +1015,7 @@ @Booklet{ Kudryashov2021 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} + year = {2021} } @InProceedings{ Kudryashov22, @@ -1006,8 +1039,7 @@ @InProceedings{ Kudryashov22 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} + complex analysis} } @InProceedings{ LeeHurLopes19, @@ -1023,8 +1055,7 @@ @InProceedings{ LeeHurLopes19 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/} + bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{ Lewis17, @@ -1040,9 +1071,7 @@ @InProceedings{ Lewis17 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{ Lewis19, @@ -1059,8 +1088,7 @@ @InProceedings{ Lewis19 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{ LewisMadelaine20, @@ -1073,8 +1101,7 @@ @InProceedings{ LewisMadelaine20 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @Article{ LewisWu22, @@ -1086,9 +1113,7 @@ @Article{ LewisWu22 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} + doi = {https://doi.org/10.1007/s10817-021-09611-1} } @InProceedings{ Limperg21, @@ -1123,8 +1148,7 @@ @InProceedings{ Limperg21 numpages = {13}, keywords = {induction, Lean, tactic, type theory, metaprogramming}, location = {Virtual, Denmark}, - series = {CPP 2021}, - tags = {about-mathlib, lean3} + series = {CPP 2021} } @InProceedings{ LimpergF23, @@ -1140,7 +1164,6 @@ @InProceedings{ LimpergF23 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} @@ -1165,16 +1188,28 @@ @InProceedings{ Livingston23 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} + homological algebra} +} + +@Article{ LS25, + title = {Formalizing zeta and {L}-functions in Lean}, + author = {David Loeffler and Michael Stoll}, + url = {https://afm.episciences.org/15328}, + doi = {10.46298/afm.15328}, + journal = {Annals of Formalized Mathematics}, + volume = {Volume 1}, + eid = 2, + year = {2025}, + month = {Jul}, + keywords = {Number Theory, Formal Languages and Automata Theory, Logic + in Computer Science} } @Article{ Madelaine19, author = {Paul{-}Nicolas Madelaine}, title = {Arithmetic and Casting in Lean}, url = {https://lean-forward.github.io/norm_cast/norm_cast.pdf}, - year = {2019}, - tags = {about-mathlib, lean3} + year = {2019} } @InProceedings{ Massot24, @@ -1197,8 +1232,7 @@ @InProceedings{ Massot24 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} + controlled natural language} } @InProceedings{ Mathlib, @@ -1213,9 +1247,7 @@ @InProceedings{ Mathlib 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{ Mehta22, @@ -1234,8 +1266,7 @@ @InProceedings{ Mehta22 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{ Mehta23, @@ -1251,12 +1282,24 @@ @InProceedings{ Mehta23 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} +} + @InProceedings{ Nash23, author = {Nash, Oliver}, title = {{A Formalisation of Gallagher’s Ergodic Theorem}}, @@ -1277,8 +1320,7 @@ @InProceedings{ Nash23 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} + Duffin-Schaeffer conjecture} } @InProceedings{ NawrockiAyersEbner23, @@ -1301,8 +1343,30 @@ @InProceedings{ NawrockiAyersEbner23 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} + Lean} +} + +@InProceedings{ norman_et_al:LIPIcs.ITP.2025.14, + author = {Norman, Chase and Avigad, Jeremy}, + title = {{Canonical for Automated Theorem Proving in Lean}}, + booktitle = {16th International Conference on Interactive Theorem + Proving (ITP 2025)}, + year = {2025}, + editor = {Forster, Yannick and Keller, Chantal}, + volume = {352}, + series = {Leibniz International Proceedings in Informatics + (LIPIcs)}, + pages = {14:1--14:20}, + address = {Dagstuhl, Germany}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + annote = {Keywords: Automated Reasoning, Interactive Theorem + Proving, Dependent Type Theory, Inhabitation, Unification, + Program Synthesis, Formal Methods}, + doi = {10.4230/LIPIcs.ITP.2025.14}, + isbn = {978-3-95977-396-6}, + issn = {1868-8969}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.14}, + urn = {urn:nbn:de:0030-drops-246128} } @InProceedings{ ObendraufBaanenKoopmanStebletsova24, @@ -1327,8 +1391,7 @@ @InProceedings{ ObendraufBaanenKoopmanStebletsova24 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} + prover} } @Article{ PNWT22, @@ -1393,8 +1456,7 @@ @Article{ PNWT22 month = jan, articleno = {47}, numpages = {28}, - keywords = {state merging, symbolic evaluation}, - tags = {formalization, lean3} + keywords = {state merging, symbolic evaluation} } @Article{ PorncharoenwasePombrioTorlak2023, @@ -1437,8 +1499,25 @@ @Article{ PorncharoenwasePombrioTorlak2023 month = oct, articleno = {261}, numpages = {28}, - keywords = {pretty printing}, - tags = {formalization, lean4} + keywords = {pretty printing} +} + +@Article{ Riou25, + title = {Formalization of derived categories in {L}ean/mathlib}, + author = {Joël Riou}, + url = {https://afm.episciences.org/13609}, + doi = {10.46298/afm.13609}, + journal = {Annals of Formalized Mathematics}, + volume = {Volume 1}, + eid = 1, + year = {2025}, + month = {Jul}, + keywords = {Derived category, Homological algebra, Spectral sequence, + MSC 2020: 18G80, 18G15, 18G40, 18E35, 68V20, + [MATH.MATH-CT]Mathematics [math]/Category Theory [math.CT], + [INFO.INFO-LO]Computer Science [cs]/Logic in Computer + Science [cs.LO]}, + language = {English} } @Article{ SelsamDeMoura16, @@ -1454,8 +1533,7 @@ @Article{ SelsamDeMoura16 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @Article{ SelsamHudonDeMoura20, @@ -1500,8 +1578,7 @@ @Article{ SelsamHudonDeMoura20 articleno = {115}, numpages = {20}, keywords = {interactive theorem proving, Lean, functional - programming}, - tags = {about-lean, lean4} + programming} } @InProceedings{ SelsamLD17, @@ -1517,8 +1594,7 @@ @InProceedings{ SelsamLD17 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @Misc{ SelsamUllrichDeMoura20, @@ -1533,17 +1609,14 @@ @Misc{ SelsamUllrichDeMoura20 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @Misc{ StricklandBellumat19, author = {Neil Strickland and Nicola Bellumat}, title = {Iterated chromatic localisation}, year = {2019}, - eprint = {arXiv:1907.07801}, - website = {https://github.com/NeilStrickland/itloc}, - tags = {formalization, lean3} + eprint = {arXiv:1907.07801} } @InProceedings{ SubercaseauxNawrockiGallicchioCodelCarneiroHeule24, @@ -1567,8 +1640,30 @@ @InProceedings{ SubercaseauxNawrockiGallicchioCodelCarneiroHeule24 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} + Geometry, Erd\H{o}s-Szekeres} +} + +@InProceedings{ tantow_et_al:LIPIcs.ITP.2025.36, + author = {Tantow, Johannes and Gerlach, Lukas and Mennicke, Stephan + and Kr\"{o}tzsch, Markus}, + title = {{Verifying Datalog Reasoning with Lean}}, + booktitle = {16th International Conference on Interactive Theorem + Proving (ITP 2025)}, + year = {2025}, + editor = {Forster, Yannick and Keller, Chantal}, + volume = {352}, + series = {Leibniz International Proceedings in Informatics + (LIPIcs)}, + pages = {36:1--36:19}, + address = {Dagstuhl, Germany}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + annote = {Keywords: Certifying Algorithms, Datalog, Formal + Verification}, + doi = {10.4230/LIPIcs.ITP.2025.36}, + isbn = {978-3-95977-396-6}, + issn = {1868-8969}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.36}, + urn = {urn:nbn:de:0030-drops-246342} } @InProceedings{ TassarottiVBT21, @@ -1598,8 +1693,7 @@ @InProceedings{ TassarottiVBT21 keywords = {probably approximately correct, interactive theorem proving, decision stumps}, location = {Virtual, Denmark}, - series = {CPP 2021}, - tags = {formalization, lean3} + series = {CPP 2021} } @Misc{ Ullrich16, @@ -1608,9 +1702,7 @@ @Misc{ Ullrich16 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} + year = {2016} } @Article{ UllrichDeMoura19, @@ -1620,8 +1712,7 @@ @Article{ UllrichDeMoura19 year = {2019}, url = {http://arxiv.org/abs/1908.05647}, archiveprefix = {arXiv}, - eprint = {1908.05647}, - tags = {about-lean, lean4} + eprint = {1908.05647} } @InProceedings{ UllrichDeMoura20, @@ -1641,8 +1732,7 @@ @InProceedings{ UllrichDeMoura20 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @Article{ UllrichDeMoura22, @@ -1658,8 +1748,7 @@ @Article{ UllrichDeMoura22 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{ VanDoornEbnerLewis20, @@ -1673,8 +1762,7 @@ @InProceedings{ VanDoornEbnerLewis20 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{ vanDoornMacbeth24, @@ -1697,8 +1785,30 @@ @InProceedings{ vanDoornMacbeth24 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} + formalized mathematics} +} + +@InProceedings{ vin_et_al:LIPIcs.ITP.2025.37, + author = {Vin, Eric and Miller, Kyle A. and Fremont, Daniel J.}, + title = {{LeanLTL: A Unifying Framework for Linear Temporal Logics + in Lean}}, + booktitle = {16th International Conference on Interactive Theorem + Proving (ITP 2025)}, + year = {2025}, + editor = {Forster, Yannick and Keller, Chantal}, + volume = {352}, + series = {Leibniz International Proceedings in Informatics + (LIPIcs)}, + pages = {37:1--37:9}, + address = {Dagstuhl, Germany}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + annote = {Keywords: Linear Temporal Logic, Interactive Theorem + Proving, Lean 4}, + doi = {10.4230/LIPIcs.ITP.2025.37}, + isbn = {978-3-95977-396-6}, + issn = {1868-8969}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.37}, + urn = {urn:nbn:de:0030-drops-246356} } @Misc{ VonRaumer15, @@ -1707,9 +1817,7 @@ @Misc{ VonRaumer15 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} + year = {2015} } @InProceedings{ VonRaumer16, @@ -1726,8 +1834,32 @@ @InProceedings{ VonRaumer16 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} + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@InProceedings{ wang_et_al:LIPIcs.ITP.2025.9, + author = {Wang, Eric and Bhoja, Arohee and Codel, Cayden and Singer, + Noah G.}, + title = {{Algebra Is Half the Battle: Verifying Presentations of + Graded Unipotent Chevalley Groups}}, + booktitle = {16th International Conference on Interactive Theorem + Proving (ITP 2025)}, + year = {2025}, + editor = {Forster, Yannick and Keller, Chantal}, + volume = {352}, + series = {Leibniz International Proceedings in Informatics + (LIPIcs)}, + pages = {9:1--9:19}, + address = {Dagstuhl, Germany}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + annote = {Keywords: Group presentations, term rewriting, + metaprogramming, proof automation, the Lean theorem + prover}, + doi = {10.4230/LIPIcs.ITP.2025.9}, + isbn = {978-3-95977-396-6}, + issn = {1868-8969}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.9}, + urn = {urn:nbn:de:0030-drops-246071} } @Article{ Wieser2021, @@ -1741,8 +1873,7 @@ @Article{ Wieser2021 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @Article{ Wieser2022, @@ -1755,9 +1886,7 @@ @Article{ Wieser2022 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} + doi = {10.1007/s00006-021-01164-1} } @InProceedings{ WieserCICM23, @@ -1773,8 +1902,7 @@ @InProceedings{ WieserCICM23 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} + doi = {10.1007/978-3-031-42753-4_15} } @InProceedings{ WieserZhang22, @@ -1793,8 +1921,7 @@ @InProceedings{ WieserZhang22 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{ WuGore19, @@ -1809,8 +1936,7 @@ @InProceedings{ WuGore19 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{ YingDegenne23, @@ -1829,8 +1955,7 @@ @InProceedings{ YingDegenne23 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} + bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{ Zhang23, @@ -1852,6 +1977,29 @@ @InProceedings{ Zhang23 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} + Proj construction, projective geometry} +} + +@InProceedings{ zhuchko_et_al:LIPIcs.ITP.2025.16, + author = {Zhuchko, Ekaterina and Maarand, Hendrik and Veanes, Margus + and Ebner, Gabriel}, + title = {{Finiteness of Symbolic Derivatives in Lean}}, + booktitle = {16th International Conference on Interactive Theorem + Proving (ITP 2025)}, + year = {2025}, + editor = {Forster, Yannick and Keller, Chantal}, + volume = {352}, + series = {Leibniz International Proceedings in Informatics + (LIPIcs)}, + pages = {16:1--16:19}, + address = {Dagstuhl, Germany}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + annote = {Keywords: Lean, regular languages, lookarounds, + derivatives, finiteness}, + doi = {10.4230/LIPIcs.ITP.2025.16}, + isbn = {978-3-95977-396-6}, + issn = {1868-8969}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.16}, + urn = {urn:nbn:de:0030-drops-246144} } +@COMMENT{jabref-meta: databaseType:bibtex;}