21
$\begingroup$

I did search on the site already and while there are questions that reference, for example, PLFA for Agda, there doesn't seem to be a canonical list of references for people just learning about proof assistants. I am looking at Isabelle/HOL: A Proof Assistant for Higher-Order Logic and Reasoning about Functional Programs - Sparkle: a Proof Assistant for Clean at the moment, but it would be nice to have some guidance as well.

I have experience with Haskell and functional programming, as well as more with C, and I'm coming to this from the direction of wondering how useful this might be in Banach Space Theory where much of the reasoning is built on well-structured normed linear spaces. So ideally I'm looking for references that describe using proof assistants with Functional Analysis and Banach Space Theory, preferably with a discussion of dual spaces and the interplay between Banach and dual spaces.

However, as the question was originally asked with less focus and obtained answers then as well, to not invalidate them, I will also accept references to books that present a strong learning path in other mathematical areas from which it is clear how to transfer the learning over to a new area (like Functional Analysis). I know proof assistants already handle linear algebra quite well, so my interest largely lies in taking that the further step to the linear functional case.

Improve this question
$\endgroup$
14
  • 3
    $\begingroup$ I have no idea why anyone would downvote this, it seems like a very valuable question. $\endgroup$
    – Neil Strickland
    Commented Feb 10, 2022 at 10:40
  • 4
    $\begingroup$ @NeilStrickland Generally, open-ended and "big list" type questions don't work well on SE sites. At the very least, this should be made into a community wiki. Also see: How to Ask Questions in Private Beta in the Help Center. $\endgroup$
    – user158
    Commented Feb 10, 2022 at 11:46
  • 2
    $\begingroup$ @postmortes I could be mistaken, but my understanding is that focus during the Private Beta should be to amass a representative sample of the kind of high-quality questions and answers that we want to invite when we open to the Public Beta mode. While it's true that at some point we would probably expect (and encourage) such a CW question to be asked and maintained, the Private Beta should most probably not be the time when this is done. $\endgroup$
    – user158
    Commented Feb 10, 2022 at 11:54
  • 3
    $\begingroup$ Eh, the edit to change the question from "Books to learn about PAs" to "Books to learn about applying PAs to specific areas of math" seems to be a huge [dareisay, breaking] shift in topics. Moreover, it'd be better to ask separately for resources applying PAs to functional analysis (or whatever specific field of math you're interested in). $\endgroup$
    – Alex Nelson
    Commented Feb 10, 2022 at 19:05
  • 1
    $\begingroup$ @AlexNelson that seems reasonable. I've made the edit. $\endgroup$
    – postmortes
    Commented Feb 10, 2022 at 19:20

9 Answers 9

Reset to default
11
$\begingroup$

The question could be summed up as a request for resources about formalizing functional analysis in proof assistants.

For this, I would recommend:

  • Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi, "Formalizing functional analysis structures in dependent type theory". e-print
  • Yasushige Watase, "Mizar Formalization of $L^{p}$ Space". Mechanized Mathematics and its Applications 8 no.1 (2010) pp.17--22, PDF

But in general, there is a severe lack of resources discussing the formalization of mathematics in a proof assistant. By this, I mean, discussing the design decisions and trade-offs, the tricks and idioms, in formalizing some given mathematical text.

Someone has been writing a Mizar Commentary on Rudin's Principles of Analysis, translating Rudin into Mizar, which can be educational. Actually, the Japanese and Chinese Mizar community has written a number of pleasant articles discussing formalizing mathematics.

But formalizing the real numbers requires care and consideration. John Harrison's PhD thesis was entirely a discussion of the costs and trade-offs of the different formalizations:

  • John Harrison, Theorem Proving with the Real Numbers. PhD thesis, also published by Springer

Original Answer for resources to learn about Proof Assistants. I'd have to advocate:

  • Nederpelt, Geuvers, and de Vrijer, Selected Papers on Automath

For type theoretic provers based on dependent types, most (if not all) the underlying concepts were invented by de Bruijn's team, and the essential papers are found here.

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ In addition to these references, I will mention my own new article (with Dupuis and Lewis), "Formalized functional analysis with semilinear maps" arxiv.org/abs/2202.05360. It's more about Hilbert spaces than Banach spaces, but it's a good place to start a reference-hunt on what Lean has in functional analysis. There's also a lot about functional analysis in Mizar (beyond that one article linked about $L^p$ spaces), and some in Isabelle. $\endgroup$
    – macbeth
    Commented Feb 14, 2022 at 16:54
  • 1
    $\begingroup$ As a random example, since you mention you're interested in duals of Banach spaces: I believe there are formalizations of the Frechet-Riesz representation theorem in Coq, Isabelle, Lean and Mizar. $\endgroup$
    – macbeth
    Commented Feb 14, 2022 at 16:55
  • 1
    $\begingroup$ @macbeth For sure, there are a lot of functional analysis formalized in Mizar! But I was looking for articles that were more like "literate programs", walking through the thought-process of formalizing functional analysis. $\endgroup$
    – Alex Nelson
    Commented Feb 14, 2022 at 16:57
13
$\begingroup$

In the Coq wiki, you'll find a list of books and tutorials which are great resources.

I personally recommend the Software foundations course (started by B. Pierce, but with many contributors over the years) where you'll both learn about Coq and logic. It's entirely written within Coq files, and you both learn how the use the tool and what it can do, through exercises of various difficulty. Finishing volumes 1 and 2 will make you a fluent user of Coq.

Improve this answer
$\endgroup$
2
  • $\begingroup$ SF is a collection of books (volumes, e.g. Volume 1 - Logical Foundations), about half a dozen of them. What do you mean by "chapters"? $\endgroup$
    – Dima Pasechnik
    Commented Feb 10, 2022 at 9:59
  • $\begingroup$ I've updated my answer to the correct terminology of "Volumes" $\endgroup$
    – cbl
    Commented Feb 10, 2022 at 10:07
12
$\begingroup$

I personally found the book Mathematical Components by Assia Mahboubi and Enrico Tassi to be the best resource for learning about Coq.

Improve this answer
$\endgroup$
10
$\begingroup$

This a bit of a roundabout suggestion, but Avigad's excellent Foundations article summarizes the variety of logics that are used to build proof assistants.

EDIT: I decided to update the post with other expositions of proof assistants / formal proof oriented to a mathematical audience.

There's a full number of the AMS Notices featuring formal proofs, with articles by Thomas Hales, Georges Gonthier, John Harrison, and Freek Wiedijk.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ I might add more info as I go remembering. In some sites SE, this makes the question “bump up” in the front page and this is frowned upon, so I'll try to be more thorough in the next update. $\endgroup$
    – Pedro Sánchez Terraf
    Commented Feb 10, 2022 at 12:00
10
$\begingroup$

For Isabelle/HOL there is the book Concrete Semantics (pdf) by Tobias Nipkow and Gerwin Klein which is a great introduction but it also covers a great deal more than just an introduction would:

  • Part I is a self-contained introduction to the proof assistant Isabelle.
  • Part II is an introduction to semantics and its applications and is based on a simple imperative programming language. It covers the following topics: operational semantics, compiler correctness, (security) type systems, program analyses, denotational semantics, Hoare logic and abstract interpretation.

I am not familiar with Isabelle/HOL: A Proof Assistant for Higher-Order Logic, so I cannot comment but I am sure it is a great book too (judging by its cover/authors).

Like Guy Coder said, the book Handbook of Practical Logic and Automated Reasoning by John Harrison which uncovers a lot of the implementation behind object logics like HOL.

Improve this answer
$\endgroup$
9
$\begingroup$

For Agda you can try Verified Functional Programming in Agda by Aaron Stump. Its first part is a rather good introduction to the language, somewhat similar to Software Foundations.

Improve this answer
$\endgroup$
9
$\begingroup$

Handbook of Practical Logic and Automated Reasoning (Site) (WorldCat) (Code and resources)

HOL Light was written by John Harrison (ref) who also authored "Handbook of Practical Logic and Automated Reasoning". Think of the book as a very detailed introduction to the code for HOL Light. (GitHub)

The book takes one from Boolean Logic all the way up to Interactive theorem proving.

I really know of no one single book that would cover proof assistants in general. So you essentially have to figure out which base for a proof assistant you want then pick a specific proof assistant then learn that one.

Another problem you may run into if this is your first time is trying to figure out if the proof assistant can do the kinds of work you need (ref), is it still supported and does it have a community site for help.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ +1 for John Harrison's book. I thought it was a beautiful read, and each chapter ends with a good "Further Reading" section. $\endgroup$
    – Alex Nelson
    Commented Feb 10, 2022 at 18:02
6
$\begingroup$

A basic introduction is the book ML for the Working Programmer by L. C. Paulson.

It is a programming book for the Standard ML language, yet it covers all the basics of functional programming, and other bits, leading to the final chapter that implements a rudimentary first-order theorem prover, called HAL.

Improve this answer
$\endgroup$
1
  • $\begingroup$ @GuyCoder I hope he is. $\endgroup$
    – tinlyx
    Commented Feb 10, 2022 at 18:27
4
$\begingroup$

I really like The Seventeen Provers of the World by Freek Wiedijk. It's a bit of a dated book (it's from 2006), however the proof assistants are pretty much the same.

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.