6
$\begingroup$

Suppose I would like to make a maths test that one can do by computer and that can be automatically checked by computer.

Question: Is there some automatic theorem prover that can check the proofs students write?

I think that, for example, Coq does not understand the body text. Or is the only possibility to write the question such that there is just one right answer for every question?

$\endgroup$
  • 6
    $\begingroup$ Automatic theorem checkers can only check proofs written according to strict syntactical rules. Few mathematicians would have the patience to write out even simple proofs that way, so I doubt students will. $\endgroup$ – Keith Jul 4 '15 at 22:31
  • $\begingroup$ I think there is software that can check computer programs written by students for correctness (and I think can also check for similarity (plagiarism)), but I am not familiar with any software that can check mathematical proofs written by students. $\endgroup$ – Joel Reyes Noche Jul 5 '15 at 0:38
  • 1
    $\begingroup$ Related to my previous comment: matheducators.stackexchange.com/q/2790/77 $\endgroup$ – Joel Reyes Noche Jul 5 '15 at 0:40
  • 2
    $\begingroup$ What level of class? With theorems and proofs being mentioned, I believe any method to do so requires more time setting up and training than actually doing it by hand. $\endgroup$ – Chris C Jul 6 '15 at 14:31
  • 1
    $\begingroup$ Slightly related were MESE 224 and MESE 1234. $\endgroup$ – Benjamin Dickman Jul 7 '15 at 0:41
3
$\begingroup$

There is no system which takes as input the pdf or .tex of a proof in natural language and check it. But there are interactive proof systems which can check some student proofs. For example there are the Lurch and Edukera.com systems. In Lurch, the student type his proof and annotate it to explain to the system where are the facts and justifications. In Edukera, you have a point and click user interface, the student can chose which theorem or logical rule to apply and the system update the current state of the textual proof.

$\endgroup$
0
$\begingroup$

One type of answer is WeBWorK

I think it cannot check proofs yet. But it can check an answer when it is a formula, rather than just a number.

$\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.