Questions on proof assistants

[Freek Wiedijk]

Dear Joe Shipman,

Let me present my take on your questions:

>My questions are:
>1) which of these can make use of work done in which other ones?

There have been, and are, many projects to make proofs from
one system available in others.  These mostly work on the
"proof term" or "basic inference" level instead of on the
"proof script" level (the level on which the user interacts
with the system), which means that the converted proofs
become huge, and not something that you would want to look at
and/or maintain.  (In Metamath there is little difference
between these two levels, which explains why Mario's
converted Metamath proofs suffer less from this problem.)

Examples of projects like this are Joe Hurd's OpenTheory,
and Gilles Dowek's Dedukti/Logipedia, but I'm sure there
are a lot more.

Also, there's the issue of alignment of definitions in
the libraries of the systems.  There also is work on
automating that, I think, but it is another barrier for
a smooth integration of the imported proofs in the system
receiving them.

The two main examples where I have seen a formalization
from a system been really used (instead of just imported
as a proof of concept of a framework) in another system is:

- Isabelle imported a lot of analysis from HOL Light.
  The original formalization was written by John Harrison,
  and the conversion was done by Larry Paulson.  I _don't_
  think this was automatic, I think Larry just "ported"
  the proofs manually by replaying John's proofs and then
  mimicking that in Isabelle.

- In Tom Hales' Flyspeck project most of the formalization
  was done in HOL Light, but an important lemma was proved
  in Isabelle by Gertrud Bauer and Tobias Nipkow.  Here the
  proof of that lemma was _not_ converted (in some sense
  it wasn't even there, not on the basic inference level),
  the statement was just "believed".  A lot of effort was
  spent here to make sure the definitions on both sides
  matched up exactly.

>2) which of these would be the easiest for mathematicians with some programming experience to learn to use to create machine-verifiable proofs?

You should ask mathematicians who did this already!
So that's Tom Hales as the main first one, and then various
people in the Lean community.  So Tom first was attracted
to HOL Light, but now is basing his Formal Abstracts
project on Lean (I'm not sure whether this still is true,
or that is he now building his own system now).  Anyway,
that seems to be pointing to Lean :-)

I personally think that a mathematician will be able to learn
any of these systems rather easily, it's not rocket science.
The biggest problem is that there is often no "mathematician
oriented" documentation available.

These systems can be used for two rather different things:

- formalizing mathematics
- formalizing computer science: both the theory of computer
  science, and the behavior of actual software/hardware

As these systems are built by computer scientists, the second
thing is what is foremost in their minds.  Which also means
that generally the people building these systems in their
documentation often presupose a familiarity with formal
logic, functional programming, lambda calculus, etc.  Or at
least they presuppose that their readers will find these
topics interesting enough to spend time getting into them :-)

Let me briefly talk about five systems.  First there are:

- HOL Light
- Mizar

The first is personally my favorite proof assistant,
because of its elegance and the amount of control it offers.
It also has a _lot_ of mathematics in its library, mostly
formalized by John.  However, it looks like a programming
language from the seventies... because it is!  The scripts
are utterly cryptic, everything is typed in capitals,
there are no tools (like for example: a user interface)
around it, etc.  Also there is not a large user community.
Finally, a weakness of all the HOL systems (including
Isabelle) is that there are no dependent types, which means
that you cannot have "abstract mathematics" so easily.

On the other hand Mizar is a mathematicians system.
Typing proofs in Mizar really feels like just doing proofs
on paper, only in a lot of _very_ small steps.  However,
Mizar has weak spots: Mizar does not allow empty types,
which means that definitions of types sometimes are not what
they should be.  There also are no binders, so you cannot
properly write things like sums and integrals, and so on.
More importantly, in Mizar there is no strong automation,
which means that everything is very manual and that can
become very tiresome.

Then there are:

- Coq
- Isabelle/HOL

Until recently these were the two serious systems.  At the
ITP conference almost all talks were about these two systems
(next to HOL4 and ACL2, but these are not so much aimed at
mathematics, so I won't talk about them here), they have
large communities, have big libraries, etc.

Now Coq has some advantages.  Most importantly it has
dependent types.  But also it has a wonderful (although
for me rather incomprehensible) proof language by Georges
Gonthier called Ssreflect, with Georges' Mathematical
Components library on top of that.  Also, two large
formalization projects by Georges, the Four Color Theorem
and the Odd Order theorem, were done using that, so it has
shown its power.  However, Coq has the handicap that it's
about constructive mathematics.  Either you add "axioms",
and then you'll be frowned on by the community (like for
instance the HoTT people :-)), or you won't be able to prove
"obvious" things.  For instance, with dependent pairs, if
<x1,x2> = <y1,y2>, in Coq it does not follow from this that
x2 = y2 (in HoTT in pairs where the second component has the
first component as its type <bool,true> = <bool,false>!)
Also, in Coq there is a difference between two flavors of
"truth values" (Prop and bool), that's what Ssreflect is for
a large part all about.  This is a bit of a hassle.

Isabelle/HOL is very different.  It has a "hammer" called
Sledgehammer, which is a big advantage, because it allows
one to find out how to do proof steps (and the lemmas need
for them!) automatically, which for a beginner is very nice.
It anyway has more of an "automated" flavor, the Isabelle
simplifier is quite powerful.  Also it's thoroughly
classical, so you won't get any "oh, but you cannot prove
that without axioms" nonsense about obvious things.  But,
as I said, it does not have dependent types.

So some years ago I said: what really needs to be there
is the "least common multiple" of Coq and Isabelle, but I
don't see that happening, these systems are _too_ different.
However, that's exactly what

- Lean

seems to become.  It's a Coq clone by Microsoft
(foo! everyone knows Microsoft is evil :-)), but the Lean
community has many hardcore former Isabelle users in it
(Jeremy Avigad, Jasmin Blanchette, etc.)  So it might be
developing into the best of both worlds.  Also, it removed
some of the subtleties of Coq that get in the way if you're
not into constructive/computable mathematics and/or Homotopy
Type Theory.  For instance, it has functional extensionality:
if f(x) = g(x) for all x then f = g; in Coq you need an axiom
for that (and also Thorsten might get angry at you :-)),
it has proof irrelevance, it has quotient types, it has a
much simpler definition of the foundations of the system
(the "logic"), etc.

Also, Patrick Massot (a geometer from Paris), told me
privately at some time that he had looked at Coq (he's
from Paris :-)), but ended up with Lean, because of the
more accessible documentation.  I think that might be
about the 173 page book by Jeremy Avigad.  So Patrick was
a mathematician similar to you, I expect.

However, Lean is a new system, so it probably has more rough
edges than Coq and Isabelle.  This also means there is less
"impressive" work in it visible yet.  The most important
is Kevin Buzzard's formalization of the _definition_ of
perfectoid spaces.   Also, there are four versions of it.
Lean 2 supports HoTT, but is obsolete.  Lean 3 is the
current version.  But there also is a Lean 4 on the horizon,
and who knows what'll happen to the libraries and community
when that arrives.  The whole thing might degenerate.
But then it might not :-)

>3) which of these have a good translator that turns a machine-readable proof into something a human reader might gain insight from?

Here the proof languages of Mizar and the Isar language
of Isabelle (based on Mizar by Makarius Wenzel) have an
advantage, I think.  They are "declarative" which means
that they have the structure of normal mathematical text.
(In Isabelle this is called "structured proof".)

Generating text from "procedural" scripts (or from the low
level proofs these generate internally), generally does not
work so well.  You get a textual proof, but not something
that a human reader would want to read.

Coq/Ssreflect is "semi-declarative", which means it can
roughly be followed without running it on a computer.
Still the scripts for it look much more like modem line
noise than the real declarative languages Mizar and Isar.

Lean can be used in a declarative way (as I said the
community has many Isabelle users, who are used to Isar).
However, from what I've seen most Lean users don't really
write their proofs in that style, Lean proofs really looks
like Coq to me.  So I'm not sure how well a declarative
proof style in Lean would work.  If it worked well, then
I would expect the mathematicians in the community to be
more attracted to it.

Anyway, these are my two cents.  I hope this is of some use,
and that I haven't offended anyone too much.

Freek