3 Search Results for "Hölzl, Johannes"

Document
DOI: 10.4230/LIPIcs.ITP.2022.10
Formalized functional analysis with semilinear maps

Authors: Frédéric Dupuis, Robert Y. Lewis, and Heather Macbeth

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

Abstract
Semilinear maps are a generalization of linear maps between vector spaces where we allow the scalar action to be twisted by a ring homomorphism such as complex conjugation. In particular, this generalization unifies the concepts of linear and conjugate-linear maps. We implement this generalization in Lean’s mathlib library, along with a number of important results in functional analysis which previously were impossible to formalize properly. Specifically, we prove the Fréchet-Riesz representation theorem and the spectral theorem for compact self-adjoint operators generically over real and complex Hilbert spaces. We also show that semilinear maps have applications beyond functional analysis by formalizing the one-dimensional case of a theorem of Dieudonné and Manin that classifies the isocrystals over an algebraically closed field with positive characteristic.
Cite as

Frédéric Dupuis, Robert Y. Lewis, and Heather Macbeth. Formalized functional analysis with semilinear maps. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dupuis_et_al:LIPIcs.ITP.2022.10,
  author =	{Dupuis, Fr\'{e}d\'{e}ric and Lewis, Robert Y. and Macbeth, Heather},
  title =	{{Formalized functional analysis with semilinear maps}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{10:1--10: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.10},
  URN =		{urn:nbn:de:0030-drops-167191},
  doi =		{10.4230/LIPIcs.ITP.2022.10},
  annote =	{Keywords: Functional analysis, Lean, linear algebra, semilinear, Hilbert space}
}
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-dev.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}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.16
Nine Chapters of Analytic Number Theory in Isabelle/HOL

Authors: Manuel Eberl

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

Abstract
In this paper, I present a formalisation of a large portion of Apostol’s Introduction to Analytic Number Theory in Isabelle/HOL. Of the 14 chapters in the book, the content of 9 has been mostly formalised, while the content of 3 others was already mostly available in Isabelle before. The most interesting results that were formalised are: - The Riemann and Hurwitz zeta functions and the Dirichlet L functions - Dirichlet’s theorem on primes in arithmetic progressions - An analytic proof of the Prime Number Theorem - The asymptotics of arithmetical functions such as the prime omega function, the divisor count sigma_0(n), and Euler’s totient function phi(n)
Cite as

Manuel Eberl. Nine Chapters of Analytic Number Theory in Isabelle/HOL. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{eberl:LIPIcs.ITP.2019.16,
  author =	{Eberl, Manuel},
  title =	{{Nine Chapters of Analytic Number Theory in Isabelle/HOL}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{16:1--16: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.16},
  URN =		{urn:nbn:de:0030-drops-110714},
  doi =		{10.4230/LIPIcs.ITP.2019.16},
  annote =	{Keywords: Isabelle, theorem proving, analytic number theory, number theory, arithmetical function, Dirichlet series, prime number theorem, Dirichlet’s theorem, zeta function, L functions}
}
  • Refine by Author
  • 2 Lewis, Robert Y.
  • 1 Dahmen, Sander R.
  • 1 Dupuis, Frédéric
  • 1 Eberl, Manuel
  • 1 Hölzl, Johannes
  • Show More...

  • Refine by Classification
  • 1 Computing methodologies → Combinatorial algorithms
  • 1 Mathematics of computing → Functional analysis
  • 1 Mathematics of computing → Mathematical analysis
  • 1 Mathematics of computing → Number-theoretic computations
  • 1 Software and its engineering → Formal methods
  • Show More...

  • Refine by Keyword
  • 2 Lean
  • 1 Dirichlet series
  • 1 Dirichlet’s theorem
  • 1 Functional analysis
  • 1 Hilbert space
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 2 2019
  • 1 2022

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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact