Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I have added both to proof and to experiment pointer to
with the quote (from p. 2):
we claim that the role of rigorous proof in mathematics is functionally analogous to the role of experiment in the natural sciences
Urs, I’m not sure how to take those additions. Do you agree with or endorse their claim?
The context of that claim seems to be a proposal of a division of labor in mathematics similar to that in physics, between theoretical physicists and experimental physicists. So a “theoretical mathematics” would be in charge of proposing speculations, conjectures, programs, and offer some plausibility or reasoning but without requiring rigorous proof, while “experimental mathematics” would be in charge of checking those by means of rigorous proof. There was also some discussion about how credit for mathematical work might be assigned.
I believe Saunders Mac Lane rejected those implications and such a proposal. Here he wrote an essay on the matter. Should such a counterbalancing opinion be added?
I went ahead and linked to the compilation of essay-responses (Atiyah et al.) to proof and experiment. I mentioned particularly Mac Lane’s reaction at proof.
Todd, I am just recording this for the same reason as I add anything else on the $n$Lab: in order to easily find it next time I need it.
Personally, the perspective that finding proof is an observational act seems to me to deeply resonate with the nature of proof in constructive mathematics, and I find it noteworthy that at least two people re-discovered this perspective in the context of mathematical physics.
Also personally, the subsequent suggestion that theoretical physics is only about speculation and not about provable fact seems misled to me. That’s why I didn’t quote that bit. But of course for historical completeness, anyone whe feels adding this should be warmly welcome to do so.
Urs: thanks for elaborating. But what had been written might have been misinterpreted by others, hence my #2 and my revision.
To me it looks as though Jaffe-Quinn understand proofs mostly in terms of validation of statements, which obviously has some truth to it but is also somewhat impoverished. Mac Lane’s remarks are a necessary corrective, and what you say in #3 is also much richer. One could go on and see formal proofs (in type theory for instance) as constructions and hence mathematical objects themselves, with internal mathematical structure, which is deeper than their role of establishing mere truth.
One could go on and see formal proofs (in type theory for instance) as constructions and hence mathematical objects themselves, with internal mathematical structure, which is deeper than their role of establishing mere truth.
That’s where I think the analogy with physical experiment is particularly neat: in both cases its about an observation that however may need an elaborate construction in order to take place.
I’ll look at MacLane’s remarks later tonight, when I have a spare minute. Thanks for amplifying this.
I went ahead and tried to incorporate some of these remarks into the article proof. Please feel free to revise.
Thanks, Todd, that looks good.
But does MacLane really object to the sentence that is currently being quoted on the $n$Lab page, or does he not rather object to the other claim, the one which I did not quote, where he writes:
Jaffe and Quinn misappropriate the word “Theoretical” as a label for what is really speculation
I suggest that after the quote currently on the $n$Lab page, we add a line such as follows:
(After making this statement about proof as observation, the article by Jaffe-Quinn goes further to suggest that the analogue in physics of speculation and conjecture in mathematics is the realm of theoretical physics, and then maybe even further in suggesting that mathematics could reasonably be purely “theoretical” in this sense. These further claims were considered faulty by several authors, but maybe in the course of rejecting them, the value of the first claim quoted above became overlooked. )
Or something like this.
Mac Lane brings up his protean idea, that a mathematical construction can be manifested in many varied ways in nature:
mathematics is that part of science which applies in more than one empirical context.
So, even if one considers an experiment as an event of a certain kind, this is still at far too great a level of specificity for him, and explains why proof is special to mathematics:
the protean character of mathematics as a part of science also explains why proofs are essential to mathematics.
I have edited and expanded a little more in the entry, accoringly. Please check out the new version here and please feel invited to disagree.
[edit: this overlapped with David’s message above]
As to #8: yes, I think he disagrees with the quoted claim, as well as with the misappropriation of the word “theoretical”. Mac Lane writes for instance (see page 15 of 29)
Their comparison of proofs in mathematics with experiments in physics is clearly faulty. Experiments may check up on a theory, but they may not be final; they depend on instrumentation, and they may even be fudged. The proof that there are infinitely many primes — and also in suitable infinite progressions — is always there.
I also wrote what I had at proof summarizing Mac Lane’s position as underlining his further tacit disagreement with that claim: experiment in physics is not considered as a final goal, and experiment is not considered as explanatory (or at least not usually).
I did some slight restructuring and put these amplifications within a Remark environment.
Thanks, Todd, I see. Thanks for your patience.
By the way, David C. and myself recently made a brief note on something related, now at
and that is really the reason why I went to track down and record the quote by Jaffe-Quinn.
In (Jaffe-Quinn 93, p. 2) it was claimed that
{#JaffeQuinnProofIsObservation} the role of rigorous proof in mathematics is functionally analogous to the role of experiment in the natural sciences
After making this statement about proof as observation,
I could imagine someone objecting to the equating of observation and experiment. Experiment tends to suggest something more of the effort to construct an instance of an event type, closer perhaps to proof as term construction.
For what it’s worth, even proofs are not always correct, and for some proofs it’s debatable whether they count as “explanatory”. Proofs are certainly different from experiments in physics in many ways, but experiments in physics are also very different from experiments in chemistry or biology. Personally, I do think of pure mathematics as an experimental science, whose subject matter is the behavior of certain formal rules, or put differently, a certain mode of functioning of a rational mind. It’s very different in many ways from most other experiemental sciences, of course, and there’s no reason that such a classification should lead us to the conclusion that it could or ought to be more similar to them in those ways; but I do think it satisfies the basic criterion. Of course, that’s just a personal point of view.
I do think of pure mathematics as an experimental science, whose subject matter is the behavior of certain formal rules, or put differently, a certain mode of functioning of a rational mind.
Thanks for saying this, Mike!
This is the kind of sentiment that I am after here.
I imagine sombody such as Martin-Löf must have expressed this sentiment before, in nicely citable form. If you remember or come across any reference, I’d be grateful for a pointer.
Alternatively, if you feel you could express it better than has been done before, I’d be happy so see you write a paragraph about it, somewhere.
Urs, I’m glad we’re having this discussion. And glad to have learned of your research proposal with David that was in the background of creating that entry; good luck with that.
Mike wrote
Personally, I do think of pure mathematics as an experimental science, whose subject matter is the behavior of certain formal rules
and I think that’s an interesting point of view.
The discussion inaugurated by Jaffe-Quinn back in that day seems to take place in a climate of alarm or worry (do we need to change journal policies, etc.) that I really don’t seem to hear much about any more. (Of course I’m somewhat removed from academic departments and academic practice, so maybe I’m just not sufficiently well-informed.)
Coming back to this after a while, I realise I had known that Peirce said something about proof and experiment in ‘The Logic of Mathematics in Relation to Education’(1898):
Kant is entirely right in saying that, in drawing those consequences,the mathematician uses what, in geometry, is called a ‘construction’, or in general a diagram, or visual array of characters or lines. Such a construction is formed according to a precept furnished by the hypothesis. Being formed, the construction is submitted to the scrutiny of observation, and new relations are discovered among its parts, not stated in the precept by which it was formed, and are found, by a little mental experimentation, to be such that they will always be present in such a construction. Thus the necessary reasoning of mathematics is performed by means of observation and experiment, and its necessary character is due simply to the circumstance that the subject of this observation and experiment is a diagram of our own creation, the condition of whose being we know all about.
But Kant, owing to the slight development which formal logic had received in his time, and especially owing to his total ignorance of the logic of relatives, which throws a brilliant light upon the whole of logic, fell into error in supposing that mathematical and philosophical necessary reasoning are distinguished by the circumstance that the former uses constructions. This is not true. All necessary reasoning whatsoever proceeds by constructions; and the difference between mathematical and philosophical necessary deductions is that the latter are so excessively simple that the construction attracts no attention and is overlooked. (CP iii. 350)
I had even quoted a part of this in a book.
Re #16,
I imagine somebody such as Martin-Löf must have expressed this sentiment before…
He does say something along these lines in Analytic and synthetic judgements in type theory, where the distinction is made between analytic judgements, such as $a:A$, and synthetic ones, such as ’$A$ is true’. The latter, an existential statement, requires “evidence resting on a construction”, which requires at least some ingenuity to find, and is not just an automatic matter of checking.
This will sound confusing to people who took from Frege that we should count as analytic anything demonstrated logically from logical axioms. He always maintained that geometric truths were synthetic a priori, but thought he’d shown arithmetic to be analytic in this sense. He did still recognise that logical reasoning could be ’ampliative’:
From this proof it can be seen that propositions that extend our knowledge can have analytic judgments for their content.
Peirce and Martin-Löf are closer to Kant in tying ’synthetic’ to the irreducible use of intuition.
1 to 19 of 19