Hi,
Il 15/08/2017 14:35, David A. Wheeler ha scritto:
> There is such a movement, any of the people participating in any of
> the formal methods systems are at least in some sense part of that.
> Freek, for example, has long been advocating for this.
>
> There are at least two problems: (1) convincing people that it is
> practical and (2) hubris.
>
> Historically the big problem with formal mathematics systems is that
> it is much more difficult to create formal proofs than informal
> proofs. That matters a lot to many mathematicians, since anything
> that makes things too difficult to publish will inhibit their ability
> to get tenure or other goodies. The continuing work to create proofs
> in metamath and other systems, as well as tools to help them, has
> been a gradual process of making it easier. Imagine trying to pray
> proofs and metamath in 1996, where a lot of the tools and proofs we
> use now were unavailable. There is reason to hope that over time it
> will slowly get easier and easier, not easy but easier.
I think this point can hardly be understressed. I am not a power
Metamath user, but when I tried it took me many hours to encode a single
"one can easily see that..." point (and it was really trivial!). There
is really a lot of implicit work under all the informal proofs that
mathematicians usually produce, many orders of magnitude. I personally
think that the routine formalization of research level maths will be
eventually possible, but we really need to achieve an impressive cut in
writing time. I would like to test whether machine learning, which made
miracles in many fields, can do something here, but have no idea of when
I will have time to test.
Another way to express the difficulty of formalizing maths is to see how
much of it has actually been formalized: a lot of great people worked on
the Metamath
set.mm, but, except in a few areas, the things in there
hardly reach the third undergraduate year (speaking in the Italian
perspective, at least). As an example (relevant from my point of view of
a differential geometer), both integration and differentiation theory
are just hinted, only in the special case of R. It is clearly
impossible, at this point, to formalize my current research work.
> Hubris is the bigger problem. Mathematicians freely admit that other
> mathematicians make mistakes, and they might be willing to admit that
> they might make a mistake. But many act in practice as if they never
> make mistakes, or that it doesn't matter if they do, because many are
> not interested in tools that can automatically check their work. Of
> course, it doesn't matter if math is just a game that you play. But
> mathematics is more than a game. Science and technology build upon
> mathematics, even in cases where people regionally thought it was
> just abstract mathematics with no applications. I would like to see
> mathematics built on much stronger and much more rigorously verified
> foundations, and I think that formal verification is a critical part
> of that.
Actually, there are many fields in which formal proving is at least
partially used to ensure safety and functionality. These fields tend to
be closer to computer science and programming than what is commonly
known as mathematics (usually I consider most of computer science a
branch of mathematics, but I think it is better to retain the
distinction here). In the case of "abstract" mathematics, the pressure
to formalization is probably much less. However, personally I would be
interested in knowing whether my PhD thesis is correct or not: I really
hope it is and I put every effort I could to make sure it was, but as I
mentioned above at the moment there is no way I can formalize it in
reasonable time (even less so considering that I would have to formalize
all its dependencies first).
I really hope to see the day in which formalizing a theorem is not much
longer than (properly) writing it in LaTeX.
My 2 cents, Giovanni.
--
Giovanni Mascellani <
g.masc...@gmail.com>
PhD Student - Scuola Normale Superiore, Pisa, Italy
http://poisson.phc.unipi.it/~mascellani