46
$\begingroup$

This question is related to (maybe even the same in intent as) Intro to automatic theorem proving / logical foundations?, but none of the answers seem to address what I'm looking for.

There are a lot of resources available for people who want to use proof assistants like Coq, Isabelle, …, to prove properties about programs—and that's no surprise, since a lot of the development of these programs is done by computer scientists. However, I am interested in resources, and especially in course materials (because I'm trying to put together an independent study for a CS student), involving the use of proof assistants to prove mathematical statements—see the work of Hales and Weedijk for examples. Does anyone know of any such?

Improve this question
$\endgroup$
1
  • 12
    $\begingroup$ Yeah, it's called graduate student! =p $\endgroup$
    – Harry Gindi
    Dec 9, 2009 at 5:51

5 Answers 5

Reset to default
10
$\begingroup$

I am interested in the same kind of stuff. This article tells about work done to formalize group representation theory in Coq. In particular, they formalize the proof of Maschke's theorem (that $F[G]$ is semisimple when $G$ is a finite group).

Some links to math courses using Coq are listed in Cocorico.

Improve this answer
$\endgroup$
21
$\begingroup$

Honestly, part of the reason that proof assistants are focused on proving programs is precisely because of our very limited understanding of how to actually represent mathematics in formal logical systems, as opposed to doing it in principle.

It turns out that program proof is basically applied metamathematics (i.e., verification of imperative programs is model theory, and verification of functional programs is structural proof theory) and this is the one area of mathematics where folks have really fully worked out in full detail how to represent what they're doing in formal logical systems. So the focus on program proof is partly making a virtue of necessity! (It's also because those of us in this area really like both programming and mathematics, and this is a great way to combine them...)

The number of people who know how to do real math in proof assistants and explain it to others can probably be counted on your fingers. A pair of suggestions to add to your list follows:

  • John Harrison wrote a recent book, Handbook of Practical Logic and Automated Reasoning, which people I trust rave about. It's a guide to all the decision procedures (e.g., SAT solving, unification, Presburger arithmetic, Groebner bases, etc.) that you need to raise the level of formal proof to a decent level of abstraction, together with their implementations in the HOL/Light system.

  • George Gonthier (who formally proved the Four Color Theorem in Coq) is currently working on formalzing the Feit-Thompson (aka Odd Order) Theorem of finite group theory. As part of this work, he and his collaborators are developing the more substantial libraries and proof automatation to support a more mathematical (as opposed to logical) style of reasoning in Coq. The guides to this work are "A Modular Formalisation of Finite Group Theory" and their Mathematical Components Library (Wayback Machine).

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ +1: "how to actually represent mathematics". I'd add a third item: De Bruijn's writings on formalising the mathematical vernacular. $\endgroup$
    – Charles Stewart
    Feb 26, 2010 at 20:07
  • $\begingroup$ +1 for mentionning de Bruijn's tremendous work in this area. The Automath papers still contain gems that few have yet to properly understand, and are reinventing all the time. $\endgroup$
    – Jacques Carette
    Feb 27, 2010 at 2:52
  • $\begingroup$ @NeelKrishnaswami , in your answer you mention that "the number of people who know how to do real math in proof assistants and explain it to others can probably be counted on your fingers". I assume you are one of them, can you list other three? what are their names? $\endgroup$
    – Jonathan Julian
    Jan 10, 2016 at 22:41
6
$\begingroup$

I would like to mention Mizar, proof verification system based on language which is human readable and very near to natural mathematical language used in mathematical practice. It is one of the longest working proof checkers, and it is one of the most successful one. Here You may find some about it: http://www.cs.ru.nl/~freek/mizar/ There is the whole library congaing presently more that 40Mb zipped proofs ( in pure ascii files!).

Improve this answer
$\endgroup$
1
6
$\begingroup$

Are you aware of the Archive of Formal Proof for Isabelle? It's a collection of formalized mathematics (and some program verification). Reading the papers there, and browsing the Isabelle theory file sources is a good way to learn.

The Isar tutorial is also a good place to look, if you want to write proofs that look like informal mathematics (as opposed to tactic style). It's quite hard to get the hang of at first (mostly due to lack of documentation), but once you get it, it's a lot easier to work with than plain lists of tactics.

If you're wanting to formalise anything with name binders (lambda-calculus, FOL, programming languages, pi-calculus, etc.) you should also check out the Nominal package for Isabelle which again helps with abstracting the proofs.

Improve this answer
$\endgroup$
4
  • $\begingroup$ Thanks --I wasn't, but Cameron Freer (mentioned above by compguy) pointed it out to me when I e-mailed him. $\endgroup$
    – LSpice
    Dec 18, 2009 at 19:58
  • 1
    $\begingroup$ Is there a way to use Isabelle without having to learn Emacs and fighting against the usual OSS problems like make scripts that don't compile? $\endgroup$
    – darij grinberg
    Feb 13, 2010 at 20:26
  • $\begingroup$ You can use Isabelle from an ML prompt. I wouldn't recommend it though. I think the Emacs frontend is going to be replaced shortly, I know there's been some work on porting ProofGeneral to the Eclipse platform. Also, I've never had a problem compiling Isabelle, even from the nightly SVN repositories. What problem are you encountering? $\endgroup$
    – user2596
    Mar 30, 2010 at 13:40
  • 1
    $\begingroup$ @darijgrinberg A little late, but the jEdit interface comes shipped by default now instead of emacs, imho this is very usable with almost no learning curve. I'm not sure if the eclipse version is still active, it's stuck on the pre 2013 version and the newest is 2015. $\endgroup$
    – simonzack
    Jul 16, 2015 at 9:45
4
$\begingroup$

The best introduction to the usage of proof assistants in mathematics that I'm personally aware of is Cameron Freer's website vdash.org. That website also links to a few resources, including the home pages of Freek Wiedijk and John Harrison, which briefly describe the usage of proof assistants in proving mathematical statements.

Unfortunately, the usability of current proof assistants seems to be extremely primitive, so introducing them in a math graduate course is going to be a challenge. You may wish to take your question to the vdash google group and/or the FOM mailing list, where some might be able to provide you with useful suggestions or unpublished lecture notes.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thanks a lot! Cameron was a student in a class I TA'd at Chicago in 1999; this is a good excuse to look him up again. $\endgroup$
    – LSpice
    Dec 18, 2009 at 19:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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