Computer assistant proofs

#1

I wonder whether TeXmacs could do some help to computer assistant proofs. For example, would it help produce a page like this one?

#2

It is something I wanted to look into. I would expect yes, but current IDEs like Visual Studio Code are very good right now in assisting writing programs for proofs assistants. It is not obvious to me what the right interface should be. Note that in the fragment you refers to, the text is just comment, the real work is done in the Lean code. I do not see much problem to reproduce this situation, but we need a way to nicely report the tactic state, maybe a side window, or a two column section of the document. Ideas are welcome.

Another interesting system is NAPROCHE which is a natural language interface to computer assistants (currently Isabelle/HOL). In NAPROCHE you write proofs in a standardised english and the computer figures out the code for the proof assistant. I saw some nice examples around.

#3

I am still not sure how exactly that works. For example, it looks like there are projects to convert Lean codes into human readable LaTeX codes.

On the other hand, about connection rather than technology, I would like to suggest a participation. This seems to be an opportunity to advertize TeXmacs. Of course, more people are working to produce LaTeX codes, but we could contact Lean teams to know what we could help to produce alternative TeXmacs output. It seems that these giant IT companies (Microsoft, Google, etc.) are quite interested in Lean, so it might be worth to try. At least, let them be aware of TeXmacs and that we are welcome to cooperations.

#4

I do not think so. My impression is that the text is a comment in the actual code. I’ve tried to write some lean proofs and they are really not very easy to read without running them in a supportive editor like Visual Studio Code.

#5

You are correct about this specific example of which the source code is available.

Lean seems to be a great star now. I saw this nature article and here is an article written by Peter Scholze. Lean succeeded to verify part of his recent work about which he had some doubts.