[FOM] shocked?

[Harvey Friedman]

I seem to be somewhat shocked that the recent thread concerning "what is a
proof" does not seem to be taking into account the rather massive literature
concerning Proof Assistants, where actual human beings actually interact
with actual computers to get humanly created proofs checked. No line by line
Hilbert style system is even remotely used in such systems. Instead, they
are based on variants of natural deduction, with an emphasis on lemma
refinement, just like most ordinary proofs humans like.

I predict that someone will find a very focused context in which one has
some very delicious notions of explanatory versus nonexplanatory proofs,
where it is mathematically rather subtle to actually show that various
statements do or do not have explanatory proofs, etcetera.

Let us compare the following two very attractive problems:

1. How do we distinguish between a proof that explains why the statement is
true, versus one that doesn't?

2. How do we tell what axioms are really needed to prove a theorem?

The big trick in f.o.m. is to figure out

which such problems are amenable to attacks that lead to rich deep
productive robust subjects with informative and sometimes surprising results
of gii?

This was done with 2 and not yet with 1. Everybody recognizes that the
present discussion of 1 is light years away from where I was with 2 already
in the late 1960's. But I do think that 1 is somewhat promising - as in the
second paragraph of this posting.

We should all agree that it is absurd to complain about, for example, 2
because it doesn't handle, for example 1.

Harvey Friedman