[FOM] formal proofs

[croux at andrew.cmu.edu]

> Thanks for this informative reply. It looks like however impressive what
we have is, there is still a lot of room for something much better in the
way of absolute rigor.
>
> I haven't really worked on this, but have the ambition to do so in the
following way. Make high level design of a "dream system" from
> scratch, first paying no attention to the present existing
> developments. This will surely lead to a number of interesting and
perhaps clean theoretical questions and theorems. Then present it to
experts in the existing practical systems, who will be able to readily
compare it to reality and criticize.
>

I would be wary of this kind of approach, as it is littered with the
corpses of many ill-conceived proof checkers.
One big issue is that what seems conceptually simple and what is
simple to implement as a proof checker are somewhat different things.

For instance, what foundational system would dream of having a complex
module system?
It seems redundant and wasteful. However, any hope of having a practical
system
needs to address this question.


> We can repeat the process using T1 and L1 again. But it would seem that
for this purpose, we may be able to lower the level of T1 and of L1, which
may be a good idea.
>
> Then we continue this process for many steps. Now are we gaining
anything by repetition here? We would if we actually get shorter and
shorter proofs in weaker and weaker L's and weaker and weaker T's. Of
course, at some point, we cannot continue to be reducing. Is there a
natural limit to such a procedure?

A natural limit is PRA, but you can probably get away with less (typically
admitting
only polynomial computable functions). Repetition is not really required:
the main potential for errors is by far in the implementation details, and
this is not
really a foundational issue, but more of a problem in computer science and
software
engineering. However, computer scientists have been verifying programs for
decades!

There have actually been a number of contributions in the area of verified
proof-checkers:

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.57.4582
http://www.cl.cam.ac.uk/~jrh13/papers/holhol.html
http://www.sciencedirect.com/science/article/pii/S157106611200028X
http://www.cs.utexas.edu/users/jared/milawa/Web/
http://dl.acm.org/citation.cfm?id=2103723&dl=ACM&coll=DL&CFID=587690589&CFTOKEN=49655975


> But we need to start somewhere to even define the problem. A purist
starting point would be primitive ZFC, where we have a claim that a given
file constitutes an absolutely correct proof of A in ZFC. Of course, since
we are working with primitive ZFC (no sugar), no human is going to even
look at this monstrosity. There is the problem of even getting a real life
math statement into primitive notation
> absolutely correctly. But I would like to separate off that question,
and take this now for granted.
>

This is the real challenge. The mental abstractions humans use when
stating and proving
theorems are extremely hard to capture, and I think this represents the
longstanding
open problem of computer-assisted verification.

More realistically, I think we should investigate manners of capturing
"field-specific" knowledge,
notations and intuition in a way that can be mechanized. It's hard for me
to think of examples,
but "working in the group of endomorphisms" in group theory comes to mind,
as well as "passing to
the dual" in linear algebra or simply just "swapping integrals" in
calculus (or swapping sums, or swapping
differentials and integrals, etc).

Just as there is no "magic bullet" in software engineering, it seems
reasonable that there is no magical
solution to the problem of mechanizing mathematics, but we have already
gone from "unthinkable" to
"possible with a massive amount of time and effort" by incremental
improvements.


> I find this whole approach rather slippery in terms of what the
> details would look like, and whether human imperfections are creeping in
in subtle ways. I need to think more deeply about this.

I'm more worried about human leaps of brilliance :)

Best,

Cody