DROPS

Document

Short Paper

DOI: 10.4230/LIPIcs.ITP.2024.40

Formalising Half of a Graduate Textbook on Number Theory (Short Paper)

Authors: Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, and Wenda Li

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract

Apostol’s Modular Functions and Dirichlet Series in Number Theory [Tom M. Apostol, 1990] is a graduate text covering topics such as elliptic functions, modular functions, approximation theorems and general Dirichlet series. It relies on complex analysis, winding numbers, the Riemann ζ function and Laurent series. We have formalised several chapters and can comment on the sort of gaps found in pedagogical mathematics. Proofs are available from https://github.com/Wenda302/Number_Theory_ITP2024.

Cite as

Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, and Wenda Li. Formalising Half of a Graduate Textbook on Number Theory (Short Paper). In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 40:1-40:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{eberl_et_al:LIPIcs.ITP.2024.40,
  author =	{Eberl, Manuel and Bordg, Anthony and Paulson, Lawrence C. and Li, Wenda},
  title =	{{Formalising Half of a Graduate Textbook on Number Theory}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{40:1--40:7},
  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.40},
  URN =		{urn:nbn:de:0030-drops-207686},
  doi =		{10.4230/LIPIcs.ITP.2024.40},
  annote =	{Keywords: Isabelle/HOL, number theory, complex analysis, formalisation of mathematics}
}

Document

DOI: 10.4230/LIPIcs.ITP.2022.11

Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics

Authors: Chelsea Edmonds and Lawrence C. Paulson

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

Abstract

The formalisation of mathematics is continuing rapidly, however combinatorics continues to present challenges to formalisation efforts, such as its reliance on techniques from a wide range of other fields in mathematics. This paper presents formal linear algebraic techniques for proofs on incidence structures in Isabelle/HOL, and their application to the first formalisation of Fisher’s inequality. In addition to formalising incidence matrices and simple techniques for reasoning on linear algebraic representations, the formalisation focuses on the linear algebra bound and rank arguments. These techniques can easily be adapted for future formalisations in combinatorics, as we demonstrate through further application to proofs of variations on Fisher’s inequality.

Cite as

Chelsea Edmonds and Lawrence C. Paulson. Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{edmonds_et_al:LIPIcs.ITP.2022.11,
  author =	{Edmonds, Chelsea and Paulson, Lawrence C.},
  title =	{{Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{11:1--11: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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.11},
  URN =		{urn:nbn:de:0030-drops-167204},
  doi =		{10.4230/LIPIcs.ITP.2022.11},
  annote =	{Keywords: Isabelle/HOL, Mathematical Formalisation, Fisher’s Inequality, Linear Algebra, Formal Proof Techniques, Combinatorics}
}

Search Results

Documents authored by Paulson, Lawrence C.

Formalising Half of a Graduate Textbook on Number Theory (Short Paper)

Abstract

Cite as

Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics

Abstract

Cite as

Thanks for your feedback!

Could not send message