Teaching logic with a proof assistant

Question

I am thinking about teaching a university-level "introduction to proofs" class (mainly for math and CS majors) making use of a computer proof assistant like Coq. I feel like there is a lot of potential benefit here, in that the students can get immediate feedback about what works and what doesn't when interacting with the proof assistant, thereby learning about the "world of mathematics" in a similar way to how a gamer learns about the world of a video game by interacting with it. However, most existing proof assistants are not really targeted at this level, so I worry that the difficulty of learning to use them could outweigh the advantages.

What experiences and research have there been with this sort of thing?

Note that I am not asking about using a proof assistant in the teaching of a class about formal logic. I know that this has been done, and experiences and research on it is not totally irrelevant to what I'm asking, but the audience is very different from a class like I'm considering; students usually already have much more mathematical maturity, and an existing understanding of what a "proof" is, coming into a formal logic class.

Edit: For further clarification, while I'm certainly interested to hear opinions and suggestions, what I'm really asking about is, as I said, experiences and research. In other words, have you or someone else done this?

Answer 1

I'm very happy to see this discussion here, because all of you are saying exactly the things that led to the project I and my collaborator (Ken Monks, Univ. Scranton) are working on, Lurch. It's free, open-source, and cross-platform, so there's no barrier to trying it out any time.

It was mentioned briefly in one of the comments above, but it's so directly related to the issues in this thread that I want to bring it up to the level of a full answer, especially since one of the other answers asserts that no such thing exists (ack!) but says he'd love to try it if it did (great!).

• The OP asks for software related to intro-to-proof courses, which are exactly the specialties Lurch focuses on, although it can do more than just those.
• He and some commenters mentioned the potential benefits of the short feedback loop, which not only is one of Lurch's strengths, but informal classroom testing confirms its value.
• The OP and one answerer also hit the nail on the head regarding the difficulty of formal syntax muddying the potential value of most proof assistants; it is for this reason that Lurch was designed to be a normal math word processor (normal math notation and typeset math built in, no funny ASCII). See the video on the Lurch homepage, linked to above.
• Finally, the OP asked only for projects that have actually been used, not just ideas; Lurch is such a project.

The discussion between the OP and @vonbrand re: many, tedious steps in formal proofs is also one of our main concerns. Lurch can handle varying levels of formality and style, and gets better at it as new versions are developed. Specific examples of what I'm talking about, with many other details, can be found in the Lurch overview whitepaper here. (That whitepaper does not cover the latest feature of math typesetting, but the video mentioned above does. The software also comes with a built-in tutorial that covers all its features.) In fact, the OP's original question, about experiences using it in class, is answered in detail, for Lurch, in that paper, for two separate courses at two different institutions.

Answer 2

This is really more of an extended comment than an answer, but I couldn't resist.

First of all, I don't know of any proof assistant that would be helpful in an "introduction to proofs" class. I would guess that no such proof assistant exists.

However, I agree that such an assistant would have the potential to be very helpful. My experience with teaching introductory proofs is that students use the following algorithm to write proofs:

1. Write an incorrect proof.

2. Turn it in, unaware of the problem

3. Find out later that it was wrong.

If I plead with the students enough to attend my office hours, this algorithm can be improved to:

1. Write an incorrect proof.

2. Show it to me. I point out that's its wrong.

3. Write a slightly better proof.

4. Show it to me. I point out that it's better but still wrong.

5. Write a correct proof.

6. Show it to me. I verify it.

7. Turn it in.

This second algorithm is of course much better, since the students actually learn to write proofs! (I cannot stress enough how important office hours are for an introductory proofs class.) Unfortunately, it's hard to have enough office hours to help all of the students through this process. What they need is an automated assistant that can check their proofs. This should be possible to program --- if there's one thing a computer ought to be able to understand, it's a proof.

To illustrate, here is a little snippet of I/O depicting a student interacting with a machine using this hypothetical program.

>>> import BasicNumberTheory
>>> begin theorem1
    >> suppose m is even
     Error: Variable 'm' not recognized!
    >> let m be an integer
    >> suppose m is even
    >> let n be an integer
    >> suppose n is even
    >> then m+n is even
    >> end theorem
>>> print theorem1
 Let m be an integer.
 Let n be an integer.
 Suppose m is even.
 Suppose n is even.
 Then m+n is even.
>>> prove theorem1
     1: m is an integer
     2: n is an integer
     3: m is even
     4: n is even
    >> By (3), m = 2j
     Error: Variable 'j' is not recognized.
    >> By (3), there exists an integer j so that m = 2j
     5: There exists an integer j so that m = 2j
    >> Let j be such
     6: j is an integer
     7: m = 2j
    >> By (4), there exists an integer k so that n = 2k
     8: There exists an integer k so that m = 2k
    >> Let k be such
     9: k is an integer
     10: n = 2k
    >> By (7) and (10), m + n = 2j + 2k
     11: m + n = 2j + 2k
    >> So m+n is even
     Error: How does this follow?
    >> So m+n = 2(j+k)
     12: m+n = 2(j+k)
    >> So m+n is even.
     Error: Missing hypothesis -- is it true that j+k is an integer?
    >> By (6) and (9), j+k is an integer
     13: j+k is an integer
    >> So m+n is even
 Proof accepted: theorem1
>>> save theorem1

I think the idea is that students would only be required to use the software for the first month or so, but I would encourage them to use it throughout the semester to check their reasoning. I'm not absolutely convinced that this would work well, but I'd love to try it!

Answer 3

I also think there might be a steep learning curve for Coq syntax. As you're referring also to CS majors, you can introduce loop invariants along with proofs by induction using the platform Why3. It is intended for deductive program verification but very few lines of code (OCaml here) are needed to demonstrate its use:

• Euclidean division
• Fast exponentiation
• Bresenham line-drawing algorithm introduced in the slides (the slide full of proof code is ironic)

If bad invariants are used, Why3 rejects the proof. If you're looking for more mathematical examples, you can use this system to prove by induction that a function computing factorials is correct, for example.

Answer 4

Maybe this is relevant for your purpose: SASyLF is an educational proof assistant for language theory:

SASyLF has a simple design philosophy: language and logic syntax, semantics, and meta-theory should be written as closely as possible to the way it is done on paper. SASyLF can express proofs typical of an introductory graduate type theory course. SASyLF proofs are generally very explicit, but its built-in support for variable binding provides substitution properties for free and avoids awkward variable encodings.

On the SASyLF webpage you can find an article describing among other things a case study from in-class use from around 2008. Currently John Boyland uses it in his Type Systems course based on Pierce's Types and programming languages. A big part of the exercises consists in writing proofs in SASyLF. I've been attending the course and found SASyLF quite easy to learn, although the documentation could be expanded.

Edit June 2016:

Some other places where logic is being taught interactively with the aid of computers:

• ProofWeb. Based coq and other proof checkers and suited among other things for use with the book Logic in Computer Science by Huth & Ryan.
• The Openproof project at Stanford's Center for the Study of Language and Information. Has several courseware packages.
• Software Foundations uses coq. Here's a talk by Benjamin Pierce about his experience with this.
• Project Ara uses the book Proof and Consequence by Jennings & Friedrich and a software called Simon.
• A introductory course on Logic an Proof by Jeremy Avigad, Robert Lewis & Floris van Doorn using Lean.

I have no personal experience with any of these but I'm adding them for completeness. Some were mentioned in this mathoverflow question.

Also there is a conference called Tools for Teaching Logic whose proceedings might contain more answers to the original question.

Answer 5

I think Coq is not the perfect tool to teach "introduction to proof" courses at entrance of university. Using Coq, impose to learn the syntax and tactics which is too demanding for introduction to proof course. For a course about logic, where you have time to focus on the formal rules of let's say natural deduction, then it is possible. I have done it with second year student.

For the "introduction to proof", I think the Edukera.com system (which is based on Coq) is more adapted, as it has a purely point and click user interface, it does not require to learn a syntax. I tried it with first year and fourth year students both could do their first proofs few minutes after starting. The drawback compared to Coq is that the teacher can not build his own exercices, and the student can not give his own definitions.

Answer 6

There's a paper available that might be relevant:

Henz, M., & Hobor, A. (2011). Teaching Experience: Logic and Formal Methods with Coq. In J.-P. Jouannaud & Z. Shao (Eds.), Certified Programs and Proofs (Vol. 7086, pp. 199–215). Berlin, Heidelberg: Springer Berlin Heidelberg. http://doi.org/10.1007/978-3-642-25379-9_16

Answer 7

You might like to look at this:

http://aim.shef.ac.uk/aim_php/html/builder_question.html

It is experimental; I have not used it with real students yet. The page gives you a selection of phrases and asks you to construct a definition of convergence by dragging and dropping. (The dragging and dropping does not work as well as it should yet; it is a bit fiddly but is OK once you get used to it.) When you click the 'Mark' button the system will critique your answer, first making sure that it can be parsed in a meaningful way, then checking whether it is actually the correct definition. Of course it would be possible to do proofs as well as definitions.

I have built a reasonably extensive Javascript framework for this kind of thing, but the logic specific to this question still takes 800 lines of code. Quite a lot of that is just blocks of LaTeX giving feedback for various types of errors. I wrote these 800 lines by hand but for a production system one would want to have some kind of GUI in which the teacher could specify the marking system in a more intuitive way.