FOM: Re: your mail

[Andrzej Trybulec]

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