7
$\begingroup$

I was wondering whether there has been any attempt to create a proof assistant that you write in it, in english,

I mean you write your proof the usual way in TeX(maybe use a 'simpler english') then instead of sending it to a journal to have it verified you use the proof assistant to have it verified for you.

There are programming languages like inform7 in which you program in english. I think what is needed is a set of macro's to turn the tex into, lets say, something that Coq can verify. Is there any such thing out there?

Do you think if this happens casual mathematicians will use it? or are there deeper problems that people don't use them now??

$\endgroup$
  • 1
    $\begingroup$ While I'm not too sure on what exactly you are asking, I feel like the series of blog posts by Tim Gowers may be of interest: gowers.wordpress.com/2013/03/25/… ; gowers.wordpress.com/2013/04/02/… ; gowers.wordpress.com/2013/04/14/… $\endgroup$ – Andrew D May 28 '13 at 9:37
  • $\begingroup$ thanks. unfortunately my internet is filtered. wordpress is not accessible in iran. do you know where else i can get this posts? i'll edit my question to make it more clear. $\endgroup$ – user76556 May 28 '13 at 12:30
  • 1
    $\begingroup$ Ah, I thought you meant a computer proving theorems in a natural language, rather than a proof checker which can check proofs in a natural language. Regardless, if you're also interested in the former, I can send you the content of the posts. $\endgroup$ – Andrew D May 28 '13 at 13:37
4
$\begingroup$

The proof-checker CalcCheck takes input via $\TeX{}$ in the form of formulas and accompanying English hints/justifications.

Given the input file, the system will output that the proof is valid at all steps or indicate which steps are poorly justified.

To the best of my knowledge, it currently recognizes most theorems of first order logic and set theory ---based on the great text ``A Logical Approach to Discrete Math.''

If I recall correctly, the back-end is in Haskell or may have already moved to Agda (a system like ${\bf Coq}$).

Main system site is at http://calccheck.mcmaster.ca/.

See $\S 5.3$ of the manual for a application, http://calccheck.mcmaster.ca/CalcCheckManual.pdf.

On a final note, this system has been used in first-year logic courses to assist students in proof-writing. It is helpful to have a system check one's proof when in-doubt.

Best regards,

Moses


Edit The above was 2013, now as of 2017, it now supports

  • creation of logical theories via named modules in the style of the Agda language
  • unicode input directly via latex-style bindings
  • "code completion" for theorem names and definitions
  • coloured and somewhat helpful error messages.

Moreover, the system now no-longer needs to be installed as an application but can be used directly via a browser.

It has been successfully used in-place of paper-and-pencil examinations at the university level with over 200 students in the 2017 fall term alone.

$\endgroup$
  • 1
    $\begingroup$ it is not exactly what i was looking for. but it seems closer than the other theorem provers to what i wanted. i'll give it a try thanks. $\endgroup$ – user76556 Jun 1 '13 at 17:47
0
$\begingroup$

There is now a program called Coqatoo that converts Coq proofs into natural-language proofs. It may be feasible to write a translator that would convert these English proofs back into Coq, but I do not know if this has been done yet.

In order to implement a natural-language theorem prover, it would be necessary to convert the input into a formal semantic representation of its meaning. The ACE reasoner was implemented in this way, using Attempto Controlled English as its input language.

$\endgroup$
-1
$\begingroup$

I believe the RISC (Research Institute for Symbolic Computation) group at Castle Hagenberg in Austria have been involved in such things for many years.

See: www.theorema.org

Based on the OP's comments below, it appears that they are not seeking an automated 'theorem prover', but an automated 'proof verifier'. If so, there is already a thread on this at:

How do proof verifiers work?

$\endgroup$
  • 1
    $\begingroup$ maybe i am wrong but it seems it is a theorem prover that generates human readable proofs. this is the opposite of what i asked. $\endgroup$ – user76556 May 26 '13 at 20:42
  • $\begingroup$ what did you ask? $\endgroup$ – wolfies May 28 '13 at 6:59
  • $\begingroup$ a proof assistant that checks the proof not generates one. but it's input is a proof written in english. like a normal tex file. it's output is either 'this proof is correct' or 'this proof is incorrect' $\endgroup$ – user76556 May 28 '13 at 9:22
  • $\begingroup$ the thread mentioned above is not exactly answering my question. it is more about HOW proof assistants work. and all that lambda calculus?, calculi? higher order logic? etc. i want to know about proof assistants from an end customer point of view, a casual mathematician. $\endgroup$ – user76556 May 30 '13 at 7:56

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.