From 340b6da52ca43731c5b92f892285e9c4eaac137e Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 13 Oct 2025 14:12:12 +0200 Subject: [PATCH 1/2] bad changes --- lean.bib | 235 +++++++++++++++++-------------------------------------- 1 file changed, 71 insertions(+), 164 deletions(-) diff --git a/lean.bib b/lean.bib index 54397077fd..fd379d0a88 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, @@ -262,8 +248,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 +271,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 +294,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 +309,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,8 +323,7 @@ @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} } @InProceedings{ Buch18, @@ -370,9 +351,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 +368,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, @@ -435,7 +413,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 +439,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 +478,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 +494,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 +516,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 +540,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 +576,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 +585,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 +603,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 +631,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 +654,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 +671,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 +710,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 +726,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 +751,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 +774,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 +790,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 +813,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, @@ -879,8 +837,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 +857,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 +867,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 +883,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 +900,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 +909,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 +921,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 +930,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 +954,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 +970,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 +986,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 +1003,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 +1016,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 +1028,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 +1063,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 +1079,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} @@ -1173,8 +1111,7 @@ @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 +1134,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 +1149,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 +1168,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,7 +1184,6 @@ @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} @@ -1277,8 +1209,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, @@ -1327,8 +1258,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 +1323,7 @@ @Article{ PNWT22 month = jan, articleno = {47}, numpages = {28}, - keywords = {state merging, symbolic evaluation}, - tags = {formalization, lean3} + keywords = {state merging, symbolic evaluation} } @Article{ PorncharoenwasePombrioTorlak2023, @@ -1454,8 +1383,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 +1428,7 @@ @Article{ SelsamHudonDeMoura20 articleno = {115}, numpages = {20}, keywords = {interactive theorem proving, Lean, functional - programming}, - tags = {about-lean, lean4} + programming} } @InProceedings{ SelsamLD17, @@ -1517,8 +1444,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 +1459,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, @@ -1598,8 +1521,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 +1530,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 +1540,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 +1560,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 +1576,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 +1590,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, @@ -1707,9 +1623,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, @@ -1741,8 +1655,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 +1668,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 +1684,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 +1703,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 +1718,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 +1737,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, From 3cd141d3ed020de22d59496bd69ed278f30698b3 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 13 Oct 2025 14:12:39 +0200 Subject: [PATCH 2/2] new papers mixed with bad changes --- lean.bib | 289 ++++++++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 265 insertions(+), 24 deletions(-) diff --git a/lean.bib b/lean.bib index fd379d0a88..16e3c33dae 100644 --- a/lean.bib +++ b/lean.bib @@ -239,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, @@ -326,6 +346,7 @@ @Article{ BrowningLutz22 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}, @@ -384,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, @@ -396,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, @@ -821,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, @@ -1103,8 +1188,21 @@ @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, @@ -1189,6 +1287,19 @@ @InProceedings{ Mehta23 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}}, @@ -1232,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, @@ -1366,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, @@ -1490,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, @@ -1613,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, @@ -1640,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, @@ -1759,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;}