Proving Theorems with Computers

[Tim Daly]

I'm leading the Axiom Computer Algebra open source
project. I've (tried to) interact with the Lean community.
I have a couple comments about your article.
https://www.ams.org/journals/notices/202011/rnoti-p1791.pdf

I wholeheartedly approve of what you are doing.
Have you video'ed any of your courses? I would
really like to take your course.



In section 3 you write
  "...I would like to discuss the possibility of teaching
   a computer pure mathematics..."

This is certainly a worthwhile goal. The current Axiom
system, however, falls into "applied mathematics" using,
as you say, "the intuition" that mathematicians develop.
It lives firmly in the "post-rigorous" stage of mathematics
despite being software.

I am trying to change that. The SANE (rational, coherent,
judicious, sound) project within Axiom has the goal of
unifying computer algebra and proof theory into a full
programming environment. Algorithms need proofs.
These proofs are "carried with them", always available
for further application.




I really wish you would write more about your comment
that "Lean is a functional programming language."




A note on the "puzzle" approach. You write
   "It is my experience that certain undergraduates
    enjoy solving puzzles like this in Lean..."
and certain of us don't. You lose the portion that
don't enjoy puzzles when they are trying to learn a
subject. Time is the only resource that is truly limited.

I, as one of the non-puzzle solvers, simply skip the
"exercise!". I'm trying to reach understanding as fast
as possible. Getting hung up because I don't know
the magic syntax and vast, inscrutable library just
wastes time.

Teaching styles differ, of course. But, unlike other
areas of mathematics, there is no other resource to
turn to when you get stuck. This is new territory.

The  fact that you consider something trivial as an
"exercise!" hearkens back to your section on "intuition".
It seems to me that you're encouraging the philosophy
you seek to undermine. Save it for the graduate level.




Axiom is also "painfully obvious" to me. It is trivial to
coerce from a Polynomial(Fraction(Integer)), which is
a polynomial with fraction coefficients, to
Fraction(Polynomial(Integer)), which is a fraction with
numerator and denominator which are polynomials
with integer coefficients. Axiom can do this in one line,
which I leave you to solve as an "exercise!".

Unfortunately, Axiom suffers from the "steep learning curve"
disease. It never caught on because the language is very
strongly typed. If you get the types wrong you'll never get
anywhere.

The point is that while you think your definition of group
in Lean is obvious (and it is, as I can "read" it), the
actual "writing" of that definition presumes a HUGE
amount of knowledge, such as type theory (Type),
class inheritance (class..extends), logic (forall),
and a deep knowledge of the libraries (has_mul,
has_one, has_inv). Further, it assume knowing where
the colons go and how to type inverse superscripts.
It also presumes knowledge about class versus theorem
as it applies to Lean.

I've been programming for 50 years and paid to program
in 60 languages. I've authored 4 commercial languages.
I can learn a "standard language" in a day. But not Lean.
"Just" getting up to speed on Type Theory costs me
8 classes with Frank Pfenning, Bob Harper, and Karl
Crary. This despite Axiom being based on types.

All of the above "presumed knowledge" to write what
appears to be something trivial that is understandable
by "any mathematician" completely ignores the huge
"learning curve", which killed Axiom. Beware.




Sure, students can solve problems that involve deeper
mathematics. I could say the same thing when I started
using the HP and TI calculators. That hardly implied
that I knew about numerical integration by false position.

Lean suffers from a lack of documentation, especially
in the library. Where would I find a section on
perfectoid rings? What is the Arzela-Ascoli theorem?

I have suggested many times (and was essentially kicked
out of the Lean forum) because I believe documentation
is vital. Indeed, I think that all of the Lean libraries ought
to be literate programs. Lean should be readable as a
textbook, with the code as "equations".

Take any math(s) textbook, delete all of the text, leaving
just the equations. Try to learn from that. That is what
Lean is doing now. Equations in textbooks are just
"pictures". All of the real knowledge is in the paragraphs.
Lean has few paragraphs. At best you get a comment.

You write Lean contains "over a quarter million lines of code".
Axiom contains 1.2 million lines of code. Axiom is
still the best implementation of the Risch Integration
algorithm. The learning curve you have to climb to
even read the integration code is a PhD degree. Oh,
and there are no comments in the code. Good luck.

It isn't obvious now but if Lean continues on this path
it will fail, just like Axiom is failing. The problem is that
once the authors leave, such as you and Mario, no-one
will be able to maintain the system. Almost all of the life
of a system is spent in maintenance. At ABSOLUTE
minimum, EVERYTHING should have a literature
bibliographic link.



You comment
  "Later on,we will ask whether proving profound results
   results like this is even the right thing to be doing"

Bruno Buchberger implemented the Groebner basis
algorithm in Axiom. Nearly 30 years later it was proven
in Coq. I applaud this effort and think it is very valuable.

However, proving the algorithm did NOT prove the
implementation. If you want to be proof theory then
"just proving" something is useful. If you want to do
computer algebra then "just implementing" something
is useful. But if you want to do "computational
mathematics", then you need to unite the two in a
deep way.

You're running hard in proof theory but you're missing
half the game.



The use of "external solvers" is close to the goal of
using computer algebra in a proof system. It would
be a great help if, for instance, you wanted a Groebner
basis solution and Axiom could provide an "answer". It would
be SO much better if the computer algebra algorithm
came back with the associated proof.



We seem to be working toward a common goal, that
of "computational mathematics". Hopefully we will
"meet in the middle".

Please, please, please video your courses.

Stay healthy. Keep up the good fight.

Tim Daly