9
$\begingroup$

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.

$\endgroup$
  • 3
    $\begingroup$ You might find the following post interesting : jiggerwit.wordpress.com/2019/06/20/… $\endgroup$ – Alex J Best Sep 30 '19 at 16:59
  • 2
    $\begingroup$ May I also suggest you spend some time reading Russell & Whitehead's Principia Mathematica? It will quickly provide some antithesis to your experience with Bourbaki, and help you to once again appreciate the advantages of natural language proofs. $\endgroup$ – Paul Sinclair Oct 1 '19 at 2:48
  • 1
    $\begingroup$ Doesn't really answer your question, but this may prove of interest: mathoverflow.net/questions/311071/… $\endgroup$ – Theoretical Economist Oct 3 '19 at 14:56
  • 2
    $\begingroup$ @PaulSinclair: Arguably, Principia was one of the first attempts, and few of the problems with it are inherent to the question. The modern approximation to the answer would probably be the Lean programming language. The subject tends to move excruciatingly slowly for decades and then to make mind-blowing quantum leaps, at least from the perspective of a semi-outsider; I wouldn't be surprised to see a natural-language version of Lean or Coq (with explicit isomorphic translation back and forth) in 5 years, ... $\endgroup$ – darij grinberg Oct 4 '19 at 16:35
  • 1
    $\begingroup$ ... nor would I be surprised if it won't arrive in the next 30. $\endgroup$ – darij grinberg Oct 4 '19 at 16:37
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I will try to get this book, thank you! Be sure I’ll keep you informed. $\endgroup$ – Blincer Oct 4 '19 at 16:57
1
$\begingroup$

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
$\endgroup$
  • $\begingroup$ These are interesting thoughts and I agree with them quite a bit, but they do not satisfy my current need for rigour. That's why I was looking for an existing tool. Maybe after all, I'll have to create such a language myself. $\endgroup$ – Blincer Oct 7 '19 at 18:58
  • $\begingroup$ @Blincer Good luck with your research project... $\endgroup$ – CopyPasteIt Oct 7 '19 at 19:00
  • $\begingroup$ Thank you very much $\endgroup$ – Blincer Oct 7 '19 at 19:01
  • $\begingroup$ @Blincer Just wondering - is the computer going to output a formal Bourbaki assembly? $\endgroup$ – CopyPasteIt Oct 7 '19 at 19:04
  • 1
    $\begingroup$ I think the best solution would be to export in Coq and secondly in LaTeX (like Bourbaki). $\endgroup$ – Blincer Oct 7 '19 at 19:07

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.