After Gentzen introduced the idea of a the sequent calculus and the idea of a Turing Machine was shown to be a complete answer to the idea of what a "computable function" is, I think the answer to the question "what is a proof" is really something along the lines of: a proof is a kind of computable function. Trying to spell out what kind of computable functions they are is a big part of one of the main outstanding problems of mathematics known as the P v NP problem. In other words, you recognize these drawings as "proofs" when you are trained to see them but nobody really knows how to define a general procedure that will output all of the correct drawings correctly (using whatever symbolism or notation you prefer). Hence the digression on proof assistants. I mean: you encounter the overall idea of producing logical drawings that demonstrate mathematical truths in elementary school geometry and then try to make those concepts more precise (as David Hilbert did) all the way through to research level mathematical logic and even then, after learning concepts that take years to master, you will still never quite know how to answer the question posed in the title of the blog post.
It's weird to me to identify proofs with a computable function that generates the steps in a sequent calculus proof. Why would this be more fundamental than the steps themselves? Even in mathematical foundations where computable functions are very important (e.g. intensional type theories like CoC) we have proof terms that are not functions (e.g. existence proofs are of sigma type, not pi type).
> Trying to spell out what kind of computable functions they are is a big part of one of the main outstanding problems of mathematics known as the P v NP problem. In other words, you recognize these drawings as "proofs" when you are trained to see them but nobody really knows how to define a general procedure that will output all of the correct drawings correctly (using whatever symbolism or notation you prefer).
P vs NP has little to do with what computable functions we consider to be proofs, if we decide to go that route at all. All proposed general mathematical foundations (ZFC, ETCS, MLTT, various HoTTs) have polynomial proof checking[1], so yes a P=NP result will mean we can check the truth of a mathematical statement in polynomial time (in the size of the proof at least), but this magic algorithm will just spit out the same form of proof that the NP verifier takes as input. This has nothing to do with what we decide to consider the format of a proof to be.
> I mean: you encounter the overall idea of producing logical drawings that demonstrate mathematical truths in elementary school geometry and then try to make those concepts more precise (as David Hilbert did) all the way through to research level mathematical logic and even then, after learning concepts that take years to master, you will still never quite know how to answer the question posed in the title of the blog post.
For particular mathematical systems, this is very much a solved problem since we have verifiers for a variety of mathematical foundations including ZFC. If you mean "what does a proof for any suitable logical system look like", we would generally require that it be some class of input that can be put into a particular computable function that is the verifier, but there is no reason to require the proof itself to be a computable function.
[1]: Yes, there are type theories with undecidable type checking but at the proof-theoretic level we would generally require the evidence that our proof term type checks to be part of the proof of a statement so this doesn't make much of a difference here.
