Here is my opinion.
Metamath is a very simple, yet very powerful and expressive language,
completely usable by both computers and humans, because it mimics/is
really close to mathematics
With a quite thin layer of tooling upon metamath, it is possible to use
it like math, but with enhancements brought by a computer and to allow :
12+ years old to do high level maths and produce computer-checked proofs.
For that, you only need to select parts of math expression with the
mouse and to select a mutation in a list of possible results. This
brings down considerably the training you need to do proper maths (and
metamath).
In the same way that calculators allow nowadays, anybody to do 1234.3657
* 578932.231 in a few seconds when it was hell in year 1560 .
Also, for professional mathematicians, it should enable them to write
their proof, export them to LaTeX (if they want) send them to research
papers, bypass the peer review process to get their research
checked/approved...and accelerate the whole damn research process, while
allowing anyone, anywhere to have access to the whole database of
mathematical discoveries
So, my answer to both questions are :
1) it is happening NOW for metamath (thanks to MathJax). When people
will look at what metamath can achieve, others (coq/lean/..) will either
throw the towel and convert or do the same thing (good luck to them,
with their otherly complex C/C++ code)
It is just a question of time (give us 1 or 2 years). People will be
able to do maths simply with the help of a computer.
2) let's build a decentralized modular database of math knowledge.
That way, people will be able to do the maths they want, the way they
want without censorship/having to conform
(I followed the discussion about metamath goals and there was quite a
lot of heat).
Ideally, I want to allow anyone to do maths the way they want and to
have what they want.
It could be done that way :
human to the tool : "use the definitions and theorems of Zfc, this
theory, that theory, category, groups, monoid"...
Tool : "done, these theorems can be used, those cannot"
Also, I am researching mm0 right now and developing a love-hate relation
with Mario's work (documentation... :/).
In the process of writing a precedence parser that handles it, I'm
understanding things.
for example, I hate precedence levels, nobody should have to learn a
precedence level, that's not how we do maths...
But, I guess that the people who don't know precedence can write
ph -> (ps -> th)
whereas the wizards (or just Mario, the wizard) will write
ph -> ps -> th
And I kinda like a lot this flexibility and that it still allows people
to do what they want/know
Also, there might be way for the tool to compute precedence levels for
the user (to avoid him the tedious parts)
like having + <. x <. ... instead of +=20 x=45
ah well stopping my rant and getting back to implementing the part about
custom notations in the mm0 parser...
Best regards,
Olivier
Le 10/02/2020 à 13:52, vvs a écrit :
He is trying to deliver this message to all, so I think people here
might be interested too:
Each formal proof verification system (Lean, Coq, Isabelle/HOL,
UniMath, all of the others) has its own community, and it is
surely in the interests of their members to see their communities
grow. These systems are all /claiming to do mathematics/, as well
as other things too (program verification, research into higher
topos theory and higher type theory etc). But two things have
become clear to me over the last two years or so:
1. There is a large community of mathematicians out there who
simply cannot join these communities because the learning
curve is too high and much of the documentation is written for
computer scientists.
2. Even if a mathematician battles their way into one of these
communities, there is a risk that they will not find the kind
of mathematics which they are being taught, or teaching, in
their own department, and there is a very big risk that they
will not find much fashionable mathematics.
My /explicit question/ to all the people in these formal proof
verification communities is: what are you doing about this?
Full post is here:
https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/
--
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/6478d27f-2d3b-4296-9f95-9236562bd7e8%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/6478d27f-2d3b-4296-9f95-9236562bd7e8%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/8828436d-f539-8562-a073-436b76334b15%40gmail.com.
