I agree with both of your view :) As for Mario's take. I am not sure that I'll be able to create a proper mock up of what could be done with Mephistolus. And It'll probably be a waste of time. So, I am just going to just coding an experimental UI for the App/Proof assistant (I'll have to do it anyway at one point).
Once it is done, it'll be easier to explain to people what can be done and what cannot (I will be able to record the Mephistolus workflow). and hopefully, I'll get good feedback to improve things afterwards. :) So, I'm going to code an UI through a single WebView, in Html/css/Javascript/MathJax/MathMl/Kotlin. And only implement the most basic math workflow (click and choose, user makes detailed decisions about expression mutations) Don't expect something fancy and polished. Let's just make something that works as expected first. :) This is going to be fun. :) Diving now in the code, see you when I have really something to display... Best regards, Olivier Le mercredi 20 novembre 2019 13:05:27 UTC+1, vvs a écrit : > > Real mathematicians don't use proof checkers, I'm afraid. It's too >> time-consuming. >> > > They will, as somebody said: "mathematics is a game", and mathematicians > like to play. Proof assistants just need a good UI to make it fun. Right > now it's boring as you already said. > -- 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/b4611d90-60e8-4a85-b11a-7fa19e6d60c9%40googlegroups.com.
