4 Search Results for "Dahmen, Sander R."

Document
Short Paper
DOI: 10.4230/LIPIcs.ITP.2023.36
Fermat’s Last Theorem for Regular Primes (Short Paper)

Authors: Alex J. Best, Christopher Birkbeck, Riccardo Brasca, and Eric Rodriguez Boidi

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
We formalise the proof of the first case of Fermat’s Last Theorem for regular primes using the Lean theorem prover and its mathematical library mathlib. This is an important 19th century result that motivated the development of modern algebraic number theory. Besides explaining the mathematics behind this result, we analyze in this paper the difficulties we faced in the formalisation process and how we solved them. For example, we had to deal with a diamond about characteristic zero fields and problems arising from multiple nested coercions related to number fields. We also explain how we integrated our work to mathlib.
Cite as

Alex J. Best, Christopher Birkbeck, Riccardo Brasca, and Eric Rodriguez Boidi. Fermat’s Last Theorem for Regular Primes (Short Paper). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 36:1-36:8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{best_et_al:LIPIcs.ITP.2023.36,
  author =	{Best, Alex J. and Birkbeck, Christopher and Brasca, Riccardo and Rodriguez Boidi, Eric},
  title =	{{Fermat’s Last Theorem for Regular Primes}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{36:1--36:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.36},
  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}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.4
Use and Abuse of Instance Parameters in the Lean Mathematical Library

Authors: Anne Baanen

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
The Lean mathematical library mathlib features extensive use of the typeclass pattern for organising mathematical structures, based on Lean’s mechanism of instance parameters. Related mechanisms for typeclasses are available in other provers including Agda, Coq and Isabelle with varying degrees of adoption. This paper analyses representative examples of design patterns involving instance parameters in the current Lean 3 version of mathlib, focussing on complications arising at scale and how the mathlib community deals with them.
Cite as

Anne Baanen. Use and Abuse of Instance Parameters in the Lean Mathematical Library. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 4:1-4:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{baanen:LIPIcs.ITP.2022.4,
  author =	{Baanen, Anne},
  title =	{{Use and Abuse of Instance Parameters in the Lean Mathematical Library}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{4:1--4:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.4},
  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}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.5
A Formalization of Dedekind Domains and Class Groups of Global Fields

Authors: Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, and Filippo A. E. Nuccio Mortarino Majno di Capriglio

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
Dedekind domains and their class groups are notions in commutative algebra that are essential in algebraic number theory. We formalized these structures and several fundamental properties, including number theoretic finiteness results for class groups, in the Lean prover as part of the mathlib mathematical library. This paper describes the formalization process, noting the idioms we found useful in our development and mathlib’s decentralized collaboration processes involved in this project.
Cite as

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)

Copy BibTex To Clipboard

@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.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}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.15
Formalizing the Solution to the Cap Set Problem

Authors: Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of F^n_q with no three-term arithmetic progression. This problem has received much mathematical attention, particularly in the case q = 3, where it is commonly known as the cap set problem. Ellenberg and Gijswijt’s proof was published in the Annals of Mathematics and is noteworthy for its clever use of elementary methods. This paper describes a formalization of this proof in the Lean proof assistant, including both the general result in F^n_q and concrete values for the case q = 3. We faithfully follow the pen and paper argument to construct the bound. Our work shows that (some) modern mathematics is within the range of proof assistants.
Cite as

Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis. Formalizing the Solution to the Cap Set Problem. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 15:1-15:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dahmen_et_al:LIPIcs.ITP.2019.15,
  author =	{Dahmen, Sander R. and H\"{o}lzl, Johannes and Lewis, Robert Y.},
  title =	{{Formalizing the Solution to the Cap Set Problem}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{15:1--15:19},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.15},
  URN =		{urn:nbn:de:0030-drops-110703},
  doi =		{10.4230/LIPIcs.ITP.2019.15},
  annote =	{Keywords: formal proof, combinatorics, cap set problem, Lean}
}
  • Refine by Author
  • 2 Baanen, Anne
  • 2 Dahmen, Sander R.
  • 1 Best, Alex J.
  • 1 Birkbeck, Christopher
  • 1 Brasca, Riccardo
  • Show More...

  • Refine by Classification
  • 2 Mathematics of computing → Mathematical software
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Type theory
  • 1 Computing methodologies → Combinatorial algorithms
  • 1 Computing methodologies → Representation of mathematical objects
  • Show More...

  • Refine by Keyword
  • 3 Lean
  • 1 Cyclotomic fields
  • 1 Fermat’s Last Theorem
  • 1 Interactive theorem proving
  • 1 Lean prover
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 1 2019
  • 1 2021
  • 1 2022
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact