Le 04/01/2020 à 21:00, vvs a écrit :
I even had some crazy thought about trying to auto generate
natural language explanations of proofs from existing proofs,
however that was probably just a flight of fancy.
Ok. Now I know. I am crazy.
And you are certainly not alone:
https://formalabstracts.github.io/
https://en.wikipedia.org/wiki/Mizar_system
Give me another 2/3 weeks and I'll demonstrate with Mephistolus preview
3 (I skipped preview 2 a week ago to make my case more convincing) that
I am also a good candidate to join the fun club of lunatics who want to
make computer generate human proofs (with some human interaction). :)
Also, I believe that there is a lot of talk in this thread about making
metamath/mm0 interface with some editor (emacs, vs studio, some
language). IMO, this is a misconception to say that it is a thread about
putting an UI on metamath
I am not sure that this is the right way to go, unless you want to
convert the process of writing maths into the art of writing software,
with features designed for software development but somehow adapted to
maths.
What about writing a standalone App DEDICATED to maths ?
see you in 2/3 weeks for less talk and more video :)
Best regards,
Olivier
--
You received this message because you are subscribed to the Google
Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send
an email to [email protected]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/b767ab62-4a42-4a6a-8289-214339bf3507%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/b767ab62-4a42-4a6a-8289-214339bf3507%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/dbaeaf45-2df0-1bef-68e8-f20b1478eaa4%40gmail.com.
