I have no wish (I'll adapt to what is available) but I have a vision :
1) Methamath (or a descendant) is the universal computer format for
maths (instead of LaTeX).
2) A proof can be exported to TeX/LaTeX/Context (pdf for print),
MathJax/html/svg/css ( for the web),
mp4/youtube (tutorials, video lessons) in 50+ human languages
3) math research is about publishing computer checkable proofs, that can
be exported to a printable proof (in any human language)
4) There is a decentralized database of what has been proven for maths,
with proofcheckers that commit/push things
(no more pear reviews, with flawed humans and all their flaws)
5) Everyone on earth can do math/research/access the knowledge base
6) there are computer games powered with a math engine that let children
enjoy themselves by solving math puzzle.
The game actually teach them useful things for life
7) math teachers write their stuff in computer checkable format instead
of TeX/LaTeX/ConTeXT
8) you can assign work to math students, they have to write computer
checkable proofs (no more grading students paper)
9) your profile on linkedin tells the math level you have achieved, so
playing games about math, can get you a job.
Ok, I may be crazy.
Still, I have started to put my master plan in motion like 1 year ago
and, to me, it looks doable so I'm making it happen ^^.
Because metamath/mm0 are already quite up to the task, the first step is
to be able to build a proof authoring tool that is good enough/great.
I fail if I cannot make expert metamathematicians (that seem to need
better tools) give up mmj2 to switch to Mephistolus.
If metamath/mm0 become even better, I will like that a lot though :)
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].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/4860658f-76ee-248c-6114-b504969c8898%40wanadoo.fr.
