4

Let us consider a quiz question whose answer is a proof. For instance, a question in mathematics, such as prove that for every natural number $n$ the quantity $n^3-n$ is even.

How could such a question be implemented in a computer interface so that the computer can check the proof for correctness?

A simple, yet unreasonable way would be to have a multiple choice format for the question, where every choice was one way of proving the relationship, but I guess the shortcomings of this are obvious...

Improve this question
5
  • 1
    Can the editor add back my initial example from physical chemistry to the post in order to avoid making the impression that I'm only interested in pure mathematics proofs, which I am not.
    – TMOTTM
    Mar 10, 2014 at 7:44
  • Feel free to add it back yourself; I didn't mean to hijack the question, but this looked like a more natural example to me (as a mathematician); not everyone is familiar with those formulas and with what it takes to manipulate them.
    – Federico Poloni
    Mar 10, 2014 at 13:42
  • 2
    I do spend some time considering what kind of statement I want to make by using a specific example, so I actually appreciate it, when the editor improves the format of a post, but it would be nice if the actual content was not changed. As seen from the discussion, changing the example considerably mis-directed several of the posters.
    – TMOTTM
    Mar 10, 2014 at 15:22
  • The main reason why I removed that example is that it was not clear at all for the reader; it contained lots of undefined variables and operators. Even if you add the definitions, people who do not know thermodynamics will get very little out of it. If you want to stick with physics, I suggest a very simple example from Newtonian mechanics.
    – Federico Poloni
    Mar 10, 2014 at 16:10
  • 1
    I agree with TMOTTM that editing out his example changes the nature of his question. The fact that it requires some subject-specific knowledge seems totally relevant in its implementation. Moreover, I would think that the best example would be the one which is closest to the type of questions the OP would actually like to implement. Anyway, one could certainly give more than one example if it seems helpful to do so.
    – Pete L. Clark
    Mar 10, 2014 at 22:18

4 Answers 4

Reset to default
6

I have experimented with a system that provides students with a collection of phrases/formulae from which they can drag and drop a selection to construct a proof. I think that this is a promising approach but there are still a large number of different ways in which students can get the answer wrong, and an even larger number of ways that they can construct an answer that cannot be parsed as something meaningful. If you simply reject such answers without comprehensible feedback then you will just make the students hate you. So you have to write a large amount of code that tries to analyse all possible answers and explain what (if anything) is wrong with them. The logic is quite complex and I am not sure how well the students would understand the explanations. I hope to return to these experiments at some point but at the moment I am not teaching anything for which they would be useful.

Improve this answer
1

It is true that a computer program cannot check the correctness of an algorithm as explained in the answer by paxinum, but that is not what is required here.

It is possible in principle for a computer to check a proof. The problem is that the proof would have to be written in a very complete form with each logical step spelt out. This is far beyond what would be required in an exam. Remember that Russel and Whitehead famously proved that 1+1=2 using 52 logical steps to finish a whole book that set up the logical formalism they would need.

In practice we write proofs with many details of the logical steps missed out and a computer would need a high level of artificial intelligence to fill in the gaps.

Neil Strickland's formulaic approach may be the best that can be done for now, but I think it would give too much away.

Improve this answer
1

There is a rich area of proof assistants which deals with these problems. See

http://coq.inria.fr/

http://wiki.portal.chalmers.se/agda/pmwiki.php

http://nuprl.org/

There is also a "market" where people can offer bitcoins for proofs checked by Coq. https://proofmarket.org/

Improve this answer
2
  • This does not really address the same problem. Unless you are teaching high level students with specific expertise in mathematical logic, it is not reasonable to ask them to write proofs that Coq will accept. Doing anything at all in Coq is orders of magnitude harder harder than writing an ordinary proof that $n^3-n$ is always even, which is the sample question that we are invited to consider.
    – Neil Strickland
    Mar 10, 2014 at 15:39
  • "Doing anything at all in Coq is orders of magnitude harder harder than writing an ordinary proof that $n^3-n$ is always even" -- That is subjective and I personally disagree. If you carefully write your "ordinary proof" without leaving any logical gaps, it won't be any significantly simpler than the Coq one.
    – Abhishek Anand
    Mar 10, 2014 at 20:18
-1

Checking proofs automatically from free-text is not something that is solved. Even if you impose very strict rules on how to type stuff, you cannot expect a program to check it.

Here is why: if your student were asked to type a computer program to solve a specific task, you cannot expect a computer program to check with 100% certainty that the algorithm is correct, in general. This is not due to technical limitations; it has been proved that there is no computer program that can guarantee that the program it checks terminate (thus is not in an infinite loop, a common error in computer science).

Hence, I suspect there will never be a generic solution to your question either.

Maybe a better from of evaluating the students is to maybe give fragments of a proof, and ask them to order these in a way that makes sense. Or even better, give the full proof, but instead ask questions about the details, with multiple-choice or simple free-form that only has a finite number of correct answers.

Improve this answer
7
  • 2
    No, checking proofs is a solved problem. See for instance en.wikipedia.org/wiki/Automated_proof_checking. It's not viable at a classroom level, but it is not an instance of the halting problem.
    – Federico Poloni
    Mar 9, 2014 at 19:42
  • Federico is right: there is a difference between submitting a program which one claims is a certain algorithm and submitting a proof in a certain formal language whose correctness can be algorithmically checked. That the latter algorithm exists is a theoretical triviality. But anyway, it seems clear that the question is about neither of these but rather something much more restricted and practical: the example given was multiple choice proofs, after all!
    – Pete L. Clark
    Mar 9, 2014 at 21:22
  • @PeteL.Clark The multiple-choice example was to illustrate how not to implement the program.
    – TMOTTM
    Mar 9, 2014 at 21:35
  • Initially, my post contained an exercise from physical chemistry. The computer would therefore also require to understand basic physics
    – TMOTTM
    Mar 9, 2014 at 21:36
  • 1
    @PeteL.Clark i did say that.. the current example is the one added by the editor of my question.
    – TMOTTM
    Mar 10, 2014 at 7:43

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .