diff --git a/lean.bib b/lean.bib index ea4ae3071..3fbf535a8 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 @InProceedings{ AGLST23, author = {Avigad, Jeremy and Goldberg, Lior and Levit, David and Seginer, Yoav and Titelman, Alon}, @@ -49,6 +47,31 @@ @InProceedings{ AngdinataXu23 tags = {formalization, lean3} } +# 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 + N\"{o}beling’s Theorem}}, + booktitle = {15th International Conference on Interactive Theorem + Proving (ITP 2024)}, + pages = {6:1--6:17}, + series = {Leibniz International Proceedings in Informatics + (LIPIcs)}, + isbn = {978-3-95977-337-9}, + issn = {1868-8969}, + year = {2024}, + volume = {309}, + editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + address = {Dagstuhl, Germany}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.6}, + urn = {urn:nbn:de:0030-drops-207347}, + doi = {10.4230/LIPIcs.ITP.2024.6}, + annote = {Keywords: Condensed mathematics, N\"{o}beling’s theorem, + Lean, Mathlib, Interactive theorem proving} +} + @Book{ Avig14, author = "Avigad, Jeremy and {de Moura}, Leonardo and Kong, Soonho", title = {{Theorem Proving in Lean}}, @@ -192,6 +215,28 @@ @Article{ BaanenDahmenNarayananNuccio22 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} +} + @Booklet{ Best2021, author = {Alexander Best}, title = {Automatically Generalizing Theorems Using Typeclasses}, @@ -225,6 +270,29 @@ @InProceedings{ BestBirkbeckBrascaRodriguez23 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} +} + @Article{ BordgCavalleri2021, author = {Anthony Bordg and Nicol{\`{o}} Cavalleri}, title = {Elements of Differential Geometry in Lean: {A} Report for @@ -352,6 +420,30 @@ @InProceedings{ Clune23 bibsource = {dblp computer science bibliography, https://dblp.org} } +@InProceedings{ CluneQianBentkampAvigad24, + author = {Clune, Joshua and Qian, Yicheng and Bentkamp, Alexander + and Avigad, Jeremy}, + title = {{Duper: A Proof-Producing Superposition Theorem Prover for + Dependent Type Theory}}, + booktitle = {15th International Conference on Interactive Theorem + Proving (ITP 2024)}, + pages = {10:1--10:20}, + series = {Leibniz International Proceedings in Informatics + (LIPIcs)}, + isbn = {978-3-95977-337-9}, + issn = {1868-8969}, + year = {2024}, + volume = {309}, + editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + address = {Dagstuhl, Germany}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.10}, + urn = {urn:nbn:de:0030-drops-207381}, + doi = {10.4230/LIPIcs.ITP.2024.10}, + annote = {Keywords: proof search, automatic theorem proving, + interactive theorem proving, Lean, dependent type theory} +} + @InProceedings{ CommelinLewis21, author = {Commelin, Johan and Lewis, Robert Y.}, title = {Formalizing the Ring of Witt Vectors}, @@ -696,6 +788,29 @@ @Article{ EURAM17 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} +} + @Misc{ FernandezMir19, author = {Ramon Fernández Mir}, title = {Schemes in Lean}, @@ -1015,6 +1130,29 @@ @Article{ Madelaine19 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} +} + @InProceedings{ Mathlib, title = {The {L}ean mathematical library}, booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International @@ -1119,6 +1257,31 @@ @InProceedings{ NawrockiAyersEbner23 tags = {about-lean, 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} +} + @Article{ PNWT22, author = {Porncharoenwase, Sorawee and Nelson, Luke and Wang, Xi and Torlak, Emina}, @@ -1334,6 +1497,30 @@ @Misc{ StricklandBellumat19 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} +} + @InProceedings{ TassarottiVBT21, author = {Tassarotti, Joseph and Vajjha, Koundinya and Banerjee, Anindya and Tristan, Jean-Baptiste}, @@ -1440,6 +1627,29 @@ @InProceedings{ VanDoornEbnerLewis20 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} +} + @Misc{ VonRaumer15, author = {Jakob {von Raumer}}, title = {Formalization of Non-Abelian Topology for Homotopy Type