[FOM] formal proofs

[Harvey Friedman]

I had no idea that the situation is more radical to the point of
claiming that traditional foundations cannot even conveniently state
"some interesting cutting edge" propositions!

For me, this makes me BOTH yet more interested in the challenge of
handling it properly in the usual f.o.m., AND more suspicious that
such things are not rigorous. In fact, I can imagine coming to the
conclusion that such things are not rigorous until it is handled
properly in the usual f.o.m. But such conclusions are of course
premature.

So again, I'll repeat my request in more focused form. We need the
simplest toy example of where there starts to be a problem in normal
formalization.

Of course, everybody involved should in principle be happy if the
material can be conveniently recast in normal foundational terms. A
priori, I'll bet that it can, using some nice key ideas of a normal
logical nature from the traditional setup that would only be obvious
to people steeped in creative f.o.m.

That's my best guess, but the burden on proof is on me. However,
"your" job is to put this in generally understandable incremental
terms, ranging from the mere hint of a foundational problem, all of
way up to the full blown situations, which many steps in between.

If "you" don't present things this way, then we don't have a good
test. Because anybody like me has no patience for anything that is not
generally understandable, and operates under the general principle
that if it is not generally understandable (statements, motivations;
not proofs, of course), then it is uninteresting. And I walk the walk,
and talk the talk.

And if you don't make it very friendly for very ignorant very skilled
very busy people like me, then we don't have a good test.

I should add that there are formalization/rigorous problems in other
very different kinds of mathematics. One is the use of "informal
probabilistic independence" that comes up in mathematical probability
theory applied to combinatorics. I remember a detailed discussion with
Joel Spencer, an expert in this. BUZZWORD: Erdos magic. I am totally
convinced that this is amenable to a very interesting normal f.o.m.
treatment. Joel definitely agrees that it represents a kind of
collapse of rigor, but not to the point of causing a collapse. He says
that a combination of people in this area (like him) being too busy
and there being no real crisis (yet), and people not having the ready
logical tools to deal with it, keep the status quo from changing. I
got interested in this, but got too busy to dig into it.

However, in "informal probabilistic independence", there doesn't seem
to be any issue of the target statements having no normal
formalization. Everything can be stated in terms of hard nosed
counting estimates.

Harvey

Urs Schreiber wrote:
> A good example of this is the formal proof, in HoTT, of the
> Blakers-Massey theorem
> (http://ncatlab.org/nlab/show/Blakers-Massey+theorem) by Lumsdaine,
> Finster and Licata. The full formalization is here:
>
>  https://github.com/dlicata335/hott-agda/blob/master/homotopy/BlakersMassey.agda
>
> I'd think that with traditional foundations even stating this theorem
> formally is impossible for all practical purposes, let alone formally
> checking its proof.
>
> In this way, there are now interesting statements in cutting edge
> algebraic/differential topology for which formalization in HoTT should
> similarly be practicable and be genuinely useful, while formalization
> of these statement in traditional foundations is possible only in
> principle. One such -- the Stokes theorem in differential generalized
> cohomology theory -- is advertized here:
>
>  https://groups.google.com/d/msg/hott-amateurs/dry16gQ8Tgo/x4_z_O7--_oJ