[FOM] formal proofs
Urs Schreiber
urs.schreiber at googlemail.com
Mon Oct 20 15:38:55 EDT 2014
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
More information about the FOM
mailing list