Technology for Which Mathematical Activities?/1

[Mario Carneiro]

On Sun, Feb 28, 2021 at 12:06 PM Harvey Friedman <hmflogic at gmail.com> wrote:

> 5. ESTABLISHING ABSOLUTE RIGOR. That, like 1, is where the technology
> has really made a difference. BUT doing this for a big theorem BEFORE
> it has really been well understood? Like - I have a pretty good idea
> of how to prove the Riemann Hypothesis maybe in about 50 pages using
> this and that this way and that way. Before I really can understand
> the details of how the subtle parts work together, I will use my proof
> assistant. I AM VERY DOUBTFUL ABOUT THIS. After the big theorem has
> been fleshed out and well understood, THEN with the technology doing
> proof verification IS GENERALLY VIABLE, although it is still
> INCREDIBLY TIME CONSUMING. WHAT ABOUT formally verifying FLT? I have
> no doubt that this will be done by 2100, but WILL INVOLVE SERIOUS
> REWORKING AND SIMPLIFICATIONS of the proof and a lot of serious time
> commitments. And the key ideas in those preliminaries are just not
> going to be using technology.
>

I do this routinely in my own research. I'm currently trying to prove a
theorem where the statement is only barely clear and the proof involves the
definitions of concepts I have only a vague grasp on. Because I'm aiming
eventually for a formal proof, I often use the proof assistant to keep my
thoughts in order, write out small proofs and make big definitions, edit
and revise; I'm still not sure any of what I've written will enter in the
final form of the theorem, but that's okay, it's just notes. Formally
checked notes, but notes nonetheless. I can do this because I have enough
experience with proof assistants that I can use them to express my
thoughts. Another mathematician in my shoes might well use latex or notepad
or good old pen and pencil to similar effect, but using a proof assistant
has its advantages. I expect that in the future, more and more people will
obtain the kind of casual familiarity with proof assistants needed to pick
it up like any other note taking tool.

To answer your question, then, how can proof assistants be used before the
proof is "dead math"? Same as any other note taking mechanism: it helps
clarify your thoughts and have more complex thoughts that will eventually
get you to the final goal. It's only as time consuming as you choose to
make it. If you don't need full rigor from the proof assistant, then don't
prove everything from scratch, just prove the parts you care about or are
unsure about. A fully formal proof is of course a much higher bar than the
proof sketches you find in mathematics journals, so it shouldn't be that
much of a surprise that it's more time consuming, but integrating the proof
assistant earlier in the process can lower the bar - if I manage to finally
make my way to the end goal, the actual formal proof will only be a matter
of stitching together the fragmented notes I've been making, rather than
some heroic voyage.

Mario Carneiro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210301/cc744c5b/attachment-0001.html>