[FOM] formal proofs

[Urs Schreiber]

On 10/16/14, Harvey Friedman <hmflogic at gmail.com> wrote:

> On Tue, Oct 14, 2014 at 10:54 AM, Josef Urban <josef.urban at gmail.com>
> wrote:
> ...
>> Voevodski describes in
>> http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf
>> several situations of recent buggy proofs and contradictory theorems
>> in his field that stayed unresolved for some time, and how he started
>> to feel uncertain about possible errors produced in "high-level" math
>> research.

[...]

> Also to get
> an idea about how high the "high-level" math is that you are referring

This notably concerns the high-level math of simplicial homotopy
theory. The HoTT foundations offers the possibility to have
*practicable* formalization of theorems and proofs in modern homotopy
theory.

A good example of this is the formal proof, in HoTT, of the
Blakers-Massy 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