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
Le 25/01/2020 à 15:04, Jon P a écrit :
I also think the future of mathematics lies in formal proofs. If there
were a database of all known proofs creating new proofs would be much
easier and more reliable. It would also reduce duplication of efforts
which must happen a lot.
One thing I think is there is probably a network effect issue. Given
there are many formal proof systems my guess is one will win out and
become the standard and then anyone who is choosing which to use will
default to that one because it is the one everyone uses.
For that reason I think things like Davids new tutorial video are very
powerful for the future of the system. Another is the idea of having a
web based editor that is easy to access.
--
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/8c7c93d9-c254-4245-8e69-f5bc34111cd5%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/8c7c93d9-c254-4245-8e69-f5bc34111cd5%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/3c24f060-30c9-5316-0e05-abe145647ae5%40gmail.com.
