6

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?

Benjamin Dickman
  • 18,470
  • 2
  • 41
  • 114
curious
  • 61
  • 1
  • 6
    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. – Keith Jul 04 '15 at 22:31
  • 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. – JRN Jul 05 '15 at 00:38
  • 1
    Related to my previous comment: http://matheducators.stackexchange.com/q/2790/77 – JRN Jul 05 '15 at 00:40
  • 2
    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. – Chris C Jul 06 '15 at 14:31
  • 1
    Slightly related were MESE 224 and MESE 1234. – Benjamin Dickman Jul 07 '15 at 00:41
  • I’ve started a prototype of something along the lines you are asking about: http://www.public-domain-materials.com/folder-student-exercise-tasks-for-mathematics-language-arts-etc---autocorrected.html – Mike Jones Oct 08 '15 at 18:26

2 Answers2

3

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.

Julien Narboux
  • 181
  • 6
0

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.

Gerald Edgar
  • 7,489
  • 1
  • 21
  • 33