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.” …

17 thoughts on “The Central Dogma of Mathematical Formalism”

Bhupinder Singh Anand

Dear Michael,

I share your prophetic vision:

`The paradigm the Hoskinson Center promises to bring into being may well be nailed in place by “eventually thousands of mathematicians or wannabe mathematicians.” I am nevertheless confident that human creativity, and the Spinozian conatus of mathematical practice, will undermine it sooner rather than later.’

Moreover, I seek to offer evidence for it in the following paper (link below), submitted to the Mathematical Proceedings of the Cambridge Philosophical Society:

Title: Why Four Colours Suffice

Subtitle: Why pre-formal ‘proofs’ entail formal proofs, and not vice versa

I’m not sure if you are aware but the term “LSD trip proof” has a long history before Jasmin Blanchette.
As far as I’m aware it comes from Scott Aaronson’s teaching statement https://www.scottaaronson.com/teaching.pdf, but has been immortalized in the published literature, by Nipkow https://dl-acm-org.vu-nl.idm.oclc.org/doi/10.1007/978-3-642-27940-9_3, here he writes about teaching Concrete Semantics, which the class at the Vrije Universiteit you link to was based on.

The Nipkow link is unfortunately only accessible to people with Vrije Universiteit credentials. Aaronson’s teaching statement is informative but mainly concerns student efforts at rigorous proofs, not proofs in published mathematical articles.

There is a long history of dissatisfaction with mathematicians on the part of computer scientists in the Netherlands. It may or may not be relevant that Amsterdam was reputed to be a very good place for LSD trips in Melkweg’s heyday, when backpackers camped out in the Vondelpark. I don’t know whether or not this reputation is still justified.

It should be pretty easy to Google for that paper “nipkow + LSD” and replace the link, unfortunately i cannot edit posts here. Alternatively just remove copy the last part.

Indeed that’s precisely the point, the origin of the term is about specifically teaching from a CS perspective, yet by quoting it you seem to take it out of context.

The context in which I found it is a project called Lean Forward which is introduced with the following justification:

The goal of the Lean Forward project is to collaborate with number theorists to formally prove theorems about research mathematics and to address the main usability issues hampering the adoption of proof assistants in mathematical circles. The theorems will be selected together with our collaborators to guide the development of formal libraries and verified tools.

Nothing is said there that suggests any connection to teaching, certainly not undergraduate students. The summary continues:

The ultimate aim is to develop a proof assistant that actually helps mathematicians…

In this context, it very much looks like the PI is proposing to help mathematicians, rather than students, write proofs that do not look like LSD trips. I am not at all convinced that mathematicians need such help.

Right you found a course on logical verification that is taught by the PI of the Lean forward project.
I don’t see any implication on the lean forward page that mathematician’s proofs look like LSD trip, which is what it sounds like you think is being said there. Simply a desire to create tools that assist mathematicians with their research.

It took me some time to realize that the best proofs should have something in common with LSD trips. Explanation tomorrow on siliconreckoner.substack.com

A proof that can’t be explained is no use. (cf. Mochizuki, passim.) The auctoritas of a machine proof depends upon (1) its comprehensibility to humans and/or (2) attestation of the integrity of the design, implementation, and execution of the logic. Of these, (2) is more meta than (1), but it could, in principle, support the auctoritas of whole classes of proofs. The open question, in my view, is whether (1) necessarily ultimately depends upon, or even must take the form of, a parallel human proof, which would then pose all of the practical and epistemological obstacles that impelled the development of machine provers in the first place.

A formal proof in practice is usually not a self-contained object but instead is a dialogue.
This is because leaders of formal theorem proving communities generally want to produce not just a series of individual proofs but a library of definitions, theorems, proofs, and proof tactics which can be combined to prove new results.

Getting a proof into such a library requires a conversation where multiple people look over it, changes are suggested, ideas are re-expressed in simplified forms, and so on. Moreover, different parts of the library play a role in this dialogue where adding new material requires older material to be rewritten, forcing results that depend on them to be rewritten as well.

Indeed this is precisely the reason why, as you mention, formal proofs can rot and degrade over time. Anything which uses the library, but doesn’t reside in it, can be broken at any point by changes in the library. So this continual dialogue between mathematicians, programmers, proofs, and programs is both the cause of (for proofs not in the library) and the solution to (for proofs in the library) this decay over time.

So the idea that a proof is a dialogue and hence formal proofs are not proofs seems, to me, untenable, at least for proofs contained in, say, Lean’s mathlib.

Your perspective on formal proof as dialogue is very congenial to me, and I would be very happy to learn that it is widely shared. It will not satisfy the philosophical tradition that sees the purpose of mathematics, and for that matter of philosophy, as the production of eternal truth. But I fear that philosophers in that tradition are doomed to eternal dissatisfaction.

“Here is the heuristic used to complete the proof by contradiction. The authors needed to show that a unitary representation of a certain group could not have an undesirable property. The (very ingenious) argument deduces from the undesirable property that one of the parameters classifying their unitary representation can be taken to be unbounded. But it is a basic principle that one of the parameters classifying the unitary representations of that group belong to a bounded set.”

“the authors’ contradiction of my Theorem 2.5.6 is not to be taken as a conclusion but rather to be bracketed within the framework of a reductio ad absurdum. ”

“it suddenly dawned on me: the sentence that had ruined my morning was in fact the conclusion of a reductio ad absurdum, or proof by contradiction! ”

Are you sure this proof uses reductio ad absurdum ? To prove that an object does not have a property, you suppose it has that property, you come to a contradiction and you can conclude.

This is basic (minimal) logic : from hypothesis P, you prove Q ans you have the conclusion : if P then Q (in your exemple Q is a contradiction, but it does not matter).

How could you do mathematics without this rule ? It is obviously correct for this “small but persistent mathematical subculture [that] rejects the law of the excluded middle, and thus the principle of proof by contradiction.”

I think it’s clear from my description that it is a proof by contradiction. I wrote “deduces from the undesirable property” and the rest of the description indicates that what is deduced is a contradiction with my Theorem 2.5.6.

Well now it is clear that you miss the distinction between :

(1) From hypothesis P, you infer a contradiction and you have the conclusion not-P.

(2) From hypothesis not-P, you infer a contradiction and you have the conclusion P.

(2) is the rule known as “reductio ad absurdum” (aka proof by contradiction). It is not the one you use according to your description. You use (1) and this is the rule sometimes called “negation-introduction”. This is basic logic ; if you do not believe me, consult an expert.

You have missed the distinction between a logic textbook and an anecdote. If I had provided the full details of the proof in the preprint you would have seen that the aim was to prove P, the strategy was to assume not-P, and the absurdity was that not-P led to a conclusion ruled out by my Theorem 2.5.6. But the anecdote would have collapsed under its own weight if I had explained that.

This is a reaction to Michael’s post “Best to equivocate on disciplinary norms” on his substack: philosophers are always wrong, great philosophers are wrong in an interesting way.
Obviously, it’s very difficult to be wrong in an interesting way.

Bhupinder Singh AnandDear Michael,

I share your prophetic vision:

`The paradigm the Hoskinson Center promises to bring into being may well be nailed in place by “eventually thousands of mathematicians or wannabe mathematicians.” I am nevertheless confident that human creativity, and the Spinozian conatus of mathematical practice, will undermine it sooner rather than later.’

Moreover, I seek to offer evidence for it in the following paper (link below), submitted to the Mathematical Proceedings of the Cambridge Philosophical Society:

Title: Why Four Colours Suffice

Subtitle: Why pre-formal ‘proofs’ entail formal proofs, and not vice versa

The subtitle says it all.

Kind regards,

Bhup

https://www.dropbox.com/s/3vzz7g4dfpsrsr8/49_Four_Colour_Submission_MPCPS_REVISION1_Epi_210923.pdf?dl=0

LikeLike

Alex J. BestI’m not sure if you are aware but the term “LSD trip proof” has a long history before Jasmin Blanchette.

As far as I’m aware it comes from Scott Aaronson’s teaching statement https://www.scottaaronson.com/teaching.pdf, but has been immortalized in the published literature, by Nipkow https://dl-acm-org.vu-nl.idm.oclc.org/doi/10.1007/978-3-642-27940-9_3, here he writes about teaching Concrete Semantics, which the class at the Vrije Universiteit you link to was based on.

LikeLike

mathematicswithoutapologiesPost authorThank you, I wasn’t aware of that!

LikeLike

mathematicswithoutapologiesPost authorThe Nipkow link is unfortunately only accessible to people with Vrije Universiteit credentials. Aaronson’s teaching statement is informative but mainly concerns student efforts at rigorous proofs, not proofs in published mathematical articles.

There is a long history of dissatisfaction with mathematicians on the part of computer scientists in the Netherlands. It may or may not be relevant that Amsterdam was reputed to be a very good place for LSD trips in Melkweg’s heyday, when backpackers camped out in the Vondelpark. I don’t know whether or not this reputation is still justified.

LikeLike

Alex BestIt should be pretty easy to Google for that paper “nipkow + LSD” and replace the link, unfortunately i cannot edit posts here. Alternatively just remove copy the last part.

Indeed that’s precisely the point, the origin of the term is about specifically teaching from a CS perspective, yet by quoting it you seem to take it out of context.

LikeLike

mathematicswithoutapologiesPost authorThe context in which I found it is a project called Lean Forward which is introduced with the following justification:

Nothing is said there that suggests any connection to teaching, certainly not undergraduate students. The summary continues:

In this context, it very much looks like the PI is proposing to help

mathematicians, rather than students, write proofs that do not look like LSD trips. I am not at all convinced that mathematicians need such help.LikeLike

Alex BestRight you found a course on logical verification that is taught by the PI of the Lean forward project.

I don’t see any implication on the lean forward page that mathematician’s proofs look like LSD trip, which is what it sounds like you think is being said there. Simply a desire to create tools that assist mathematicians with their research.

LikeLike

mathematicswithoutapologiesPost authorThe quotation about the LSD trip comes from one of the documents on the Lean Forward page.

LikeLike

mathematicswithoutapologiesPost authorIt took me some time to realize that the best proofs should have something in common with LSD trips. Explanation tomorrow on siliconreckoner.substack.com

LikeLike

frankwilhoitA proof that can’t be explained is no use. (

cf. Mochizuki,passim.) Theauctoritasof a machine proof depends upon (1) its comprehensibility to humans and/or (2) attestation of the integrity of the design, implementation, and execution of the logic. Of these, (2) is more meta than (1), but it could, in principle, support theauctoritasof whole classes of proofs. The open question, in my view, is whether (1) necessarily ultimately depends upon, or even must take the form of, a parallel human proof, which would then pose all of the practical and epistemological obstacles that impelled the development of machine provers in the first place.LikeLike

williamsawinA formal proof in practice is usually not a self-contained object but instead is a dialogue.

This is because leaders of formal theorem proving communities generally want to produce not just a series of individual proofs but a library of definitions, theorems, proofs, and proof tactics which can be combined to prove new results.

Getting a proof into such a library requires a conversation where multiple people look over it, changes are suggested, ideas are re-expressed in simplified forms, and so on. Moreover, different parts of the library play a role in this dialogue where adding new material requires older material to be rewritten, forcing results that depend on them to be rewritten as well.

Indeed this is precisely the reason why, as you mention, formal proofs can rot and degrade over time. Anything which uses the library, but doesn’t reside in it, can be broken at any point by changes in the library. So this continual dialogue between mathematicians, programmers, proofs, and programs is both the cause of (for proofs not in the library) and the solution to (for proofs in the library) this decay over time.

So the idea that a proof is a dialogue and hence formal proofs are not proofs seems, to me, untenable, at least for proofs contained in, say, Lean’s mathlib.

LikeLike

mathematicswithoutapologiesPost authorYour perspective on formal proof as dialogue is very congenial to me, and I would be very happy to learn that it is widely shared. It will not satisfy the philosophical tradition that sees the purpose of mathematics, and for that matter of philosophy, as the production of eternal truth. But I fear that philosophers in that tradition are doomed to eternal dissatisfaction.

LikeLike

Maurice aaabeYou write

“Here is the heuristic used to complete the proof by contradiction. The authors needed to show that a unitary representation of a certain group could not have an undesirable property. The (very ingenious) argument deduces from the undesirable property that one of the parameters classifying their unitary representation can be taken to be unbounded. But it is a basic principle that one of the parameters classifying the unitary representations of that group belong to a bounded set.”

“the authors’ contradiction of my Theorem 2.5.6 is not to be taken as a conclusion but rather to be bracketed within the framework of a reductio ad absurdum. ”

“it suddenly dawned on me: the sentence that had ruined my morning was in fact the conclusion of a reductio ad absurdum, or proof by contradiction! ”

Are you sure this proof uses reductio ad absurdum ? To prove that an object does not have a property, you suppose it has that property, you come to a contradiction and you can conclude.

This is basic (minimal) logic : from hypothesis P, you prove Q ans you have the conclusion : if P then Q (in your exemple Q is a contradiction, but it does not matter).

How could you do mathematics without this rule ? It is obviously correct for this “small but persistent mathematical subculture [that] rejects the law of the excluded middle, and thus the principle of proof by contradiction.”

Best,

Maurice

LikeLike

mathematicswithoutapologiesPost authorI think it’s clear from my description that it is a proof by contradiction. I wrote “deduces from the undesirable property” and the rest of the description indicates that what is deduced is a contradiction with my Theorem 2.5.6.

LikeLike

Maurice aaabeWell now it is clear that you miss the distinction between :

(1) From hypothesis P, you infer a contradiction and you have the conclusion not-P.

(2) From hypothesis not-P, you infer a contradiction and you have the conclusion P.

(2) is the rule known as “reductio ad absurdum” (aka proof by contradiction). It is not the one you use according to your description. You use (1) and this is the rule sometimes called “negation-introduction”. This is basic logic ; if you do not believe me, consult an expert.

Best,

Maurice

LikeLike

mathematicswithoutapologiesPost authorYou have missed the distinction between a logic textbook and an anecdote. If I had provided the full details of the proof in the preprint you would have seen that the aim was to prove P, the strategy was to assume not-P, and the absurdity was that not-P led to a conclusion ruled out by my Theorem 2.5.6. But the anecdote would have collapsed under its own weight if I had explained that.

LikeLike

Anthony BordgThis is a reaction to Michael’s post “Best to equivocate on disciplinary norms” on his substack: philosophers are always wrong, great philosophers are wrong in an interesting way.

Obviously, it’s very difficult to be wrong in an interesting way.

LikeLike