natural language proof assistant

Question

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??

Answer 1

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?

Answer 2

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.

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

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.

---

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.

Unfortunately, it is not open source.