For mathematical formalists, a proof is a sequence of valid formulas in a symbolic language, each obtained from the previous one (more likely the conjunction of several) by a legal transformation (rule of deduction), or the statement of an axiom.
A theorem is then any valid formula that appears as the final statement in a sequence.
Here is a recent
militant but unsubstantiated attempt to ventriloquize mathematics in support of this Central Dogma:
an informal mathematical statement is a theorem if and only if its formal counterpart has a formal derivation. Whether or not a mathematician reading a proof would characterize the state of affairs in these terms, a judgement as to correctness is tantamount to a judgment as to the existence of a formal derivation, and whatever psychological processes the mathematician brings to bear, they are reliable insofar as they track the correspondence. (Jeremy Avigad, 2020)
Avigad, as you see, actually writes “if and only if.” …
The distinction between “if” and “only if” is in any case lost on the public when the Dogmatic position is supported, as Avigad’s is, by a new $20,000,000 institute as well as the backing of a 33-year-old cryptocurrency billionaire who is rumored to be willing to donate ten times as much over the coming years.…
The complete essay can be read on the Silicon Reckoner Substack newsletter. Comments welcome here.