Re: [mizar] A quote

[Freek Wiedijk <freek@cs.kun.nl>]

Hi Piotr,

>I welcome your paper as it may attract working
>mathematicians towards computerized proof assistants: Mizar,
>Coq, Isabelle or whatever,

Let's specify the "or whatever".  I always have _six_ systems
in mind that are serious contenders here:

  Coq
  NuPRL/MetaPRL
  Mizar
  Isabelle/Isar
  HOL/HOL Light
  PVS
  
You might claim that Isabelle/HOL and HOL are the same
system, but to me they're sufficiently different.

Systems I left out:

  Metamath
    nice but too basic (and I don't like they way the ignore
    alpha conversion)
  IMPS
    would be in this list if it still was an active project
  MathScheme
    will be in this list when it matures, I suppose
  ACL2
    a great system but the language is not expressive enough
    for abstract math

>However, Mizar library seems to be largest of such and I
>think that building such a library is the main challenge,

For me another challenge is to get formalization time down.
I claim that currently it takes on average about one week to
formalize one page from a math textbook.  To develop
technology that brings that time down to (say) one day,
that's important too.  Maybe even more important than the
challenge you mention.

Freek