The paper On Gödel's theorems on lengths of proofs I: Number of lines and speedup for arithmetics contains quite interesting results on proof length. But some of the details are still, to me, a bit fuzzy [I now find a lot of non-formalized mathematics a bit fuzzy, an occupational hazard it seems].

There is a somewhat related thread on here, but it doesn't link to machine-checked formalizations.

  • 1
    $\begingroup$ I don’t follow formalized mathematics, but it’s extremely unlikely. In this field, pretty much nothing at all has been formalized. $\endgroup$ Dec 14, 2019 at 7:33


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.