Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
David Kurniadi Angdinata and Junyan Xu. An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{angdinata_et_al:LIPIcs.ITP.2023.6, author = {Angdinata, David Kurniadi and Xu, Junyan}, title = {{An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {6:1--6:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-284-6}, ISSN = {1868-8969}, year = {2023}, volume = {268}, editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.6}, 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} }
Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
María Inés de Frutos-Fernández. Formalizing Norm Extensions and Applications to Number Theory. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{defrutosfernandez:LIPIcs.ITP.2023.13, author = {de Frutos-Fern\'{a}ndez, Mar{\'\i}a In\'{e}s}, title = {{Formalizing Norm Extensions and Applications to Number Theory}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {13:1--13:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-284-6}, ISSN = {1868-8969}, year = {2023}, volume = {268}, editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.13}, URN = {urn:nbn:de:0030-drops-183880}, doi = {10.4230/LIPIcs.ITP.2023.13}, annote = {Keywords: formal mathematics, Lean, mathlib, algebraic number theory, p-adic analysis, Galois representations, p-adic Hodge theory} }
Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
Amelia Livingston. Group Cohomology in the Lean Community Library. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{livingston:LIPIcs.ITP.2023.22, author = {Livingston, Amelia}, title = {{Group Cohomology in the Lean Community Library}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {22:1--22:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-284-6}, ISSN = {1868-8969}, year = {2023}, volume = {268}, editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.22}, URN = {urn:nbn:de:0030-drops-183974}, doi = {10.4230/LIPIcs.ITP.2023.22}, annote = {Keywords: formal math, Lean, mathlib, group cohomology, homological algebra} }
Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
Oliver Nash. A Formalisation of Gallagher’s Ergodic Theorem. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{nash:LIPIcs.ITP.2023.23, author = {Nash, Oliver}, title = {{A Formalisation of Gallagher’s Ergodic Theorem}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {23:1--23:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-284-6}, ISSN = {1868-8969}, year = {2023}, volume = {268}, editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.23}, URN = {urn:nbn:de:0030-drops-183981}, doi = {10.4230/LIPIcs.ITP.2023.23}, annote = {Keywords: Lean proof assistant, measure theory, metric number theory, ergodicity, Gallagher’s theorem, Duffin-Schaeffer conjecture} }
Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
Jujian Zhang. Formalising the Proj Construction in Lean. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 35:1-35:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{zhang:LIPIcs.ITP.2023.35, author = {Zhang, Jujian}, title = {{Formalising the Proj Construction in Lean}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {35:1--35:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-284-6}, ISSN = {1868-8969}, year = {2023}, volume = {268}, editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.35}, URN = {urn:nbn:de:0030-drops-184105}, doi = {10.4230/LIPIcs.ITP.2023.35}, annote = {Keywords: Lean, formalisation, algebraic geometry, scheme, Proj construction, projective geometry} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Yaël Dillies and Bhavik Mehta. Formalising Szemerédi’s Regularity Lemma in Lean. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{dillies_et_al:LIPIcs.ITP.2022.9, author = {Dillies, Ya\"{e}l and Mehta, Bhavik}, title = {{Formalising Szemer\'{e}di’s Regularity Lemma in Lean}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {9:1--9:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-252-5}, ISSN = {1868-8969}, year = {2022}, volume = {237}, editor = {Andronick, June and de Moura, Leonardo}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.9}, URN = {urn:nbn:de:0030-drops-167185}, doi = {10.4230/LIPIcs.ITP.2022.9}, annote = {Keywords: Lean, formalisation, formal proof, graph theory, combinatorics, additive combinatorics, Szemer\'{e}di’s Regularity Lemma, Roth’s Theorem} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
María Inés de Frutos-Fernández. Formalizing the Ring of Adèles of a Global Field. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{defrutosfernandez:LIPIcs.ITP.2022.14, author = {de Frutos-Fern\'{a}ndez, Mar{\'\i}a In\'{e}s}, title = {{Formalizing the Ring of Ad\`{e}les of a Global Field}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {14:1--14:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-252-5}, ISSN = {1868-8969}, year = {2022}, volume = {237}, editor = {Andronick, June and de Moura, Leonardo}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.14}, 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} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, and Filippo A. E. Nuccio Mortarino Majno di Capriglio. A Formalization of Dedekind Domains and Class Groups of Global Fields. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{baanen_et_al:LIPIcs.ITP.2021.5, author = {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni and Nuccio Mortarino Majno di Capriglio, Filippo A. E.}, title = {{A Formalization of Dedekind Domains and Class Groups of Global Fields}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {5:1--5:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.5}, URN = {urn:nbn:de:0030-drops-139004}, doi = {10.4230/LIPIcs.ITP.2021.5}, annote = {Keywords: formal math, algebraic number theory, commutative algebra, Lean, mathlib} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Kevin Buzzard. What Makes a Mathematician Tick? (Invited Talk). In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{buzzard:LIPIcs.ITP.2019.2, author = {Buzzard, Kevin}, title = {{What Makes a Mathematician Tick?}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {2:1--2:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.2}, URN = {urn:nbn:de:0030-drops-110576}, doi = {10.4230/LIPIcs.ITP.2019.2}, annote = {Keywords: Formalization of mathematics} }
Feedback for Dagstuhl Publishing