[FOM] 603: Removing Deep Pathology 3 (Harvey Friedman)

[Colin McLarty]

On Tue, Aug 25, 2015 at 10:33 PM, Timothy Y. Chow <tchow at alum.mit.edu>
wrote (with much else):

>
> There is a *very weak* correlation between uniform/conceptual proofs and
> short proofs.  The latter is of course easy to analyze formally,
>
> Actually I think shortness of proofs is not easy to analyze formally in a
way that will apply to most of mathematical practice.

Proof length in formal theories is sensitive to the vocabulary of the
theory.   This is well understood when it comes to worst case bounds on
length of proofs in ZFC versus in Goedel-Bernays set theory.  It is widely
and reasonably believed that such speed up is not so extreme for most of
the theorems that mathematicians use most of the time  -- but I do not
believe this idea has been made precise and I doubt that would be easy to
do,

It gets worse as we go farther from foundational theories,  Finite group
theorists certainly believe the introduction of apt technical ideas like
"thin group" shortens proofs. In some sense it obviously does, but I doubt
this is well understood at all on a formal level.  I would be happy to
learn of references showing it is well understood formally, of course, but
I doubt it is.

Colin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150826/b3a0225e/attachment.html>