FOM: Re: your mail
Andrzej Trybulec
trybulec at math.uwb.edu.pl
Mon Apr 12 09:19:42 EDT 1999
On Mon, 29 Mar 1999, Harvey Friedman wrote:
> Basically, the Mizar project **suggests** (not proves!) that formalization
> can actually be carried out by human beings with the help of computers for
> all of published mathematics, and gives us some idea of how long this would
> take."
>
> Could you comment on the second paragraph to the FOM?
OK
I use "footnotes" ( "*...*"), I think not everybody is interested in details.
It is an experiment and it proves nothing, at least if we use "to prove" in
the mathematical meaning. But even if "to prove" is used in colloquial sense
the results that we have got still does not prove that
published mathematics is formalizable because the amount of mathematics
formalized in Mizar is not big enough (*).
Still, I believe that it is more than suggestion. Actually I am convinced (**)
(not certain) that the formalization of the whole published mathematics
is (virtually) possible.
With two reservations:
1. I doubt if it can be done with Mizar as it is now. (***)
The further development of the language is necessary. However,
most of the problems related seems to be rather linguistic ones rather
than logical.
2. There are mathematical papers that hardly are formalizable.
- Some of them use strong geometrical insight
and some facts in them are not proved, but a picture is provided instead.
For instance, we need two representation of a polyhedron, one
to prove that it is embeddable in E^3, just draw a picture, the other
as a CW-complex to prove homotopy properties. And because the fact
that it is the same polyhedron (up to the homeomorphism) is easy
to see, so it is not proved.
With the (computer generated) movies one can use the visualization
even for much more complicated arguments.
- The computation (more and more often used) may be quite difficult
to formalize.
Both phenomena are somewhat related, we substitute for the proof
an experiment.
Let me mention two other problems:
When we have defined a function, and from the definition is obvious
how to compute it, we do not prove that it is recursive (I owe this
example to Staszek Krajewski). And the proof may be very long and
tedious.
Quite often some metamathematical arguments are used. It is typical
in the case of the isomorphism theorems. Let me give less obvious
example. Let G = <X, t, m> a topological group and T = <X, t>
the corresponding topological space. G is compact iff T is compact.
Obvious, isn't it? How to prove it?
The time needed for formalization is extremely difficult to estimate.
Proving Hahn-Banach theorem took 3 days, if I recall. On the other
hand the proof of the Jordan curve theorem we started in 1991 and
as yet it is proved only for polygonal curves (actually a special case:
for polygons with edges parallel to axes).
=====================================================================
(*) Recently we are concentrated on three directions:
- The prove of the Jordan curve theorem, it is a challenge because
it needs a lot of facts about plane (topology, analytic geometry).
At least the proof that we are formalizing.
- The formalization of the theory of continuous lattices. We follow
"A Compendium of Continuous Lattices" (G.Gierz, K.H.Hofmann, K.Keimel,
J.D.Lawson, M.Mislove, D.S.Scott), about 30% is already
formalized. (****)
I do not want you to misconstrue what I wrote, we omit
examples, some of them need mathematics that would take more
time that anything already done, if we tried to formalize it.
It is a challenge because it needs uniform formalization of many
facts (when we formalize a separate theorem, quite often we choose
such formalization that is convenient for the author, not for somebody
that want to use it).
- A theory of abstract computers. The theory of programs (as a mathematical
objects) has been developed. Properties of simple programs are proved
(computing Fibonacci numbers, bubble sort)
(**) Not because the technology developed in 1989 was sufficient, in the
meantime the language (and the system) evolved quite fast. And not
because we were able to enhance the system and it still can be used.
The reason is that, I believe, the enhancements consist in
the reconstruction of mechanisms used in mathematics. So I hope
that with a complete reconstruction of the mathematical language
the formalization will be feasible.
(***) I mean the language itself. Maybe the more important is the data base.
In the case of the theory of continuous lattices the size of text
that includes the formalization of the theory presented in the book
and the size of the text necessary to bridge the existing data base
are of the same order.
(****)
We were extremely lucky with the choice of the book. The "A Compendium .."
is very rigorous. We found one misprint, few shortcomings and,
maybe, one real mistake.
Andrzej Trybulec
More information about the FOM
mailing list