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$ – Emil Jeřábek Dec 14 '19 at 7:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.