# Are there automatic solution checkers?

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?

• 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 4 '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. – Joel Reyes Noche Jul 5 '15 at 0:38
• Related to my previous comment: matheducators.stackexchange.com/q/2790/77 – Joel Reyes Noche Jul 5 '15 at 0:40
• 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 6 '15 at 14:31
• Slightly related were MESE 224 and MESE 1234. – Benjamin Dickman Jul 7 '15 at 0:41