26
$\begingroup$

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?

|improve this question|||||
$\endgroup$
  • 5
    $\begingroup$ I think this is an excellent idea. Perhaps the main obstacle that most students have in a proofs course is that they don't get enough feedback on their written proofs -- they need to have the ability to "compile" a proof and receive error messages. A simple computer proof assistant for doing basic proofs in something close to natural language would be ideal, though I don't know whether such a system exists. $\endgroup$ – Jim Belk Mar 15 '14 at 22:49
  • $\begingroup$ One hurdle I see is that "people" proofs are much less formal. If students see themselves having to write down lots of "useless, obvious" stuff in some arcane language, it could be a big turn-off. $\endgroup$ – vonbrand Mar 16 '14 at 17:26
  • 1
    $\begingroup$ @vonbrand, I actually think that's a benefit, although the students may not see it as such. In my experience it's often the stuff that people (especially experts) consider "obvious" that trips up beginners; forcing them to write it down in the beginning will give them a more solid understanding of what's going on, so that later on they can start omitting it without confusing themselves. $\endgroup$ – Mike Shulman Mar 17 '14 at 5:54
  • 2
    $\begingroup$ This sort of discussion is much improved by the presence of data. (-: Which is why I asked the question... $\endgroup$ – Mike Shulman Mar 18 '14 at 4:36
  • 1
    $\begingroup$ Lurch may also be of interest. $\endgroup$ – J W May 29 '14 at 20:13
10
$\begingroup$

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.

|improve this answer|||||
$\endgroup$
  • $\begingroup$ This is excellent! Although Lurch is not exactly a proof assistant of the sort I had in mind, it is similar enough to have many of the same benefits (and others that I didn't consider). However, one benefit that I had in mind is in an area where Lurch specifically differs from the proof assistants I'm familiar with, namely its restriction to what in the paper you call "explicit validation". I had thought that it would be useful for students to be able to "explore the world" of mathematical proofs in a gamelike way, learning the rules by seeing what is possible, but ... $\endgroup$ – Mike Shulman Jun 18 '14 at 4:48
  • $\begingroup$ ... while you give students experience with "implicit validation" in the "Toy Proofs" systems, you graduate to explicit validation at the same time as you move to actual mathematics. Often two new things at once is difficult, so I would have considered doing mathematics with implicit validation (such as a traditional proof assistant) in between. Why did you made the choice you did? Does it have to do with the comment on p17 that in the early version of Lurch with implicit validation it was more possible to do a proof by trial and error without thinking? $\endgroup$ – Mike Shulman Jun 18 '14 at 4:49
  • $\begingroup$ Yes, students' (self-reported) ability to make valid proofs without understanding what was going on was high with implicit validation, and low with explicit validation. But that wasn't our specific motivation for dropping implicit validation. Rather, part of our mission is that writing math in Lurch should be VERY much like writing math elsewhere; thus Lurch should have a familiar, word-processor UI, as opposed to being a game. (Math games can have benefits, but Lurch is a word processor.) $\endgroup$ – Nathan Jun 20 '14 at 15:11
8
$\begingroup$

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!

|improve this answer|||||
$\endgroup$
  • 1
    $\begingroup$ I want this hypothetical program to exist, and would happily help work on it if it was a real project. $\endgroup$ – Chris Cunningham♦ Mar 17 '14 at 8:48
  • 1
    $\begingroup$ This is more or less exactly what I'm envisioning. It is, of course, possible to have essentially the same interaction with an existing proof assistant, so I'm curious why you think none such would work; is it just the barrier of syntax? $\endgroup$ – Mike Shulman Mar 17 '14 at 15:24
  • $\begingroup$ @MikeShulman Yes. For a program that students use (especially students with no programming experience), the interface ought to be close to natural language, and the error messages need to be clear. I've never seen a proof assistant with these properties, though I'd be delighted to learn that one exists. $\endgroup$ – Jim Belk Mar 17 '14 at 15:33
  • $\begingroup$ This is why I want to hear about someone who's actually tried it. I don't want to underestimate students, who are often more technologically savvy than we give them credit for. I also think there may be ways to make the proof assistant's "native" syntax and error messages more comprehensible, e.g. by explicitly teaching BHK/PAT as a way to understand the rules of proof. $\endgroup$ – Mike Shulman Mar 18 '14 at 4:39
  • $\begingroup$ @MikeShulman: In addition to the syntax barrier, I'd be very worried about the installation barrier. Hopefully Coq is better, but just getting Agda installed on student's computers would take the first month of a class. Similarly, you'd want a program that didn't require understanding Emacs, knowing what a command line is, etc. Otherwise you're going to be spending the first month just going over background. Most of today's college students have never seen a command line. $\endgroup$ – Noah Snyder Apr 2 '14 at 21:47
3
$\begingroup$

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:

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.

|improve this answer|||||
$\endgroup$
  • $\begingroup$ Interesting, thanks! However, at first sight this looks much too CS-y for my math majors. There are CS students in the class, but it's a math class. In particular, I want a system that students can use with their very first, simplest, proofs -- proving that a function computing factorials is correct is way more advanced. $\endgroup$ – Mike Shulman Mar 17 '14 at 5:49
  • $\begingroup$ (Also, what I'm really looking for with this particular question is experiences, not suggestions.) $\endgroup$ – Mike Shulman Mar 17 '14 at 5:52
3
$\begingroup$

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:

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.

|improve this answer|||||
$\endgroup$
2
$\begingroup$

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

|improve this answer|||||
$\endgroup$
1
$\begingroup$

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.

|improve this answer|||||
$\endgroup$
  • $\begingroup$ Interesting; thanks! (Of course, it's not what the question is about.) $\endgroup$ – Mike Shulman Mar 17 '14 at 15:26
  • 1
    $\begingroup$ The functionality given in the builder_question.html example is currently available in beta form for the online homework system WeBWorK (using the draggableProof macro). $\endgroup$ – Paul Pearson Mar 17 '14 at 23:51
1
$\begingroup$

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.

|improve this answer|||||
$\endgroup$
0
$\begingroup$

You may find interesting mathdialog.com it is friendly, very close to the mathematics textbooks language and formal at the same time.

|improve this answer|||||
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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