Controlled natural language for mathematics

Question

I am a French student very inspired by Bourbaki's but I can no longer stand to write approximate proofs. I was wondering if there was a language between formal and natural language that was both non-binding for the reader (he or she had nothing to learn to read the demonstration) and mechanical enough to be understood by a computer.

I found two or three projects but no clear documentation.

To be precise, I don't mind that the project is abandoned as long as there is an exhaustive (and high level) description of the syntax.

Answer 1

I recommend reading "Book of Proof" $2009$ by Richard H. Hammack. Hardcover is only about $25$ USD and it describes the language (mostly natural) to be used in proofs. It shows how to address the reader as though in a conversation: "We can see that...". It also shows some mathematical symbols used in proofs but mostly, it's how to approach a proof by induction or whatever with examples.

I don't know how a proof would fit in a computer but it appears that PYTHON is the preferred language for doing math stuff. On the other hand, there is a movement to have machines both write and validate proofs. I don't know the language but it is described in "Mathematics without Apologies: Portrait of a Problematic Vocation (Science Essentials)" $2015$ by Michael Harris.

If you find what you are looking for, give us an update. I'm sure that many people would be interested.

Answer 2

I don't believe what you are looking for will ever be developed.

In the future mathematicians will be able to write down a proof sketch or hypothesis in their natural language of choice (French is certainly a beautiful language) and then get the details or rejection from an AI machine.

The IBM Watson computer is good with natural language and you can imagine it playing an intermediate role. The two of you get along OK and can easily talk math together. Watson then speaks to a Google AI machine that is a mathematician extraordinaire. It get backs to Watson in a couple of seconds, who then speaks to you about the results.

From

$\quad$ Google AI system proves over 1200 mathematical theorems

you'll find the following quote,

You get the maximum of precision and correctness all really spelled out, but you don’t have to do the work of filling in the details. … Maybe offloading some things that we used to do by hand frees us up for looking for new concepts and asking new questions.

• Jeremy Avigad