Theoretical Mathematics

Stream: general

[Tim Daly]

Thurston has an interesting paper (Thurston, William P. "On Proof and Progress in Mathematics",Bull. AMS, v30 n2 April 1994) (https://arxiv.org/pdf/math/9404236.pdf) on page 3 he caricatures what mathematicians do as:

D. mathematicians start from a few basic mathematical structures and a collection of axioms "given" about those structures, that

T. There are various important questions to be answered about these structures that can be stated as formal mathematical propositions, and

P. the task of the mathematician is to seek a deductive pathway from the axioms to the propositions or to their denials.

All, in all, an interesting paper to read.

[Joe]

Though it seems to me that this is the model which he aims to criticize in that paper, and he argues in the rest of the paper that mathematical understanding is something very different from this so-called definition-theorem-proof (DTP) model of mathematics.

[Tim Daly]

Indeed, he goes on to say "I am NOT criticizing the mathematical study of formal proofs, nor am I criticizing people who put energy into making mathematical arguments more explicit and more formal."

[Tim Daly]

He also says "There are people working hard on the project of actually formalizing parts of mathematics by computer, with actual formally correct formal deductions. I think this is a very big but very worthwhile project."

[Tim Daly]

But he also stresses that communication is central to the game. As a rabid follower of Knuth's Literate Programming path I feel that it is important to document the theorems with an emphasis on communication. The bare Lean code is not sufficient.

[Kevin Buzzard]

The reason I am interested in formalising things is that I believe that mathematics is a bit out of control and I am concerned that we are publishing unjustified results. I fear that the problem will get worse over time. I absolutely appreciate Thurston's point of view but I think that when papers of my colleagues announce new results which depend on (a) unpublished work and (b) work which in my opinion has not been checked carefully enough by experts, then I begin to lose trust in it. My community however does not. This is independent of Thurston's main point, which is that doing new mathematics involves creativity and some kind of model of what is going on.

Whenever someone brings up Thurston's article now I always tell them to not to forget to read the article by Jaffe and Quinn which it was responding to (and which implicitly criticises Thurston for not giving enough proof details for one of the major claims he made).

[Kevin Buzzard]

I could also add that mathematics has moved a long way since the mid-90s. Fermat's Last Theorem is just at the boundary of what one person can really understand, but it could only rely on 30 years of deep algebraic geometry because that's all the human race had had time to construct by then. Things are worse now. Stuff gets simplified and new stuff appears, and the shapes of proofs change, but ultimately it seems to me that things just rely on more and more and more material.

[Joe Hendrix]

Thanks for sharing the Jaffe and Quinn paper; that seemed pretty sensible to me. I especially agree with the part about papers claiming they've proven results, but not actually having complete proofs, but since the result is proven there is little incentive to try to make a more rigorous proof. There's definitely been a few topics in CS that I've stayed away from because the accepted papers don't seem to have a correct proof (or at least have inferences that I can't follow), but also I can't find a counterexample stating the theorem is wrong.

[Joe Hendrix]

I was curious how mathematicians using Lean feel about this claim in the Thurston paper "The standard of correctness and completeness necessary to get a computer program to work at all is a couple of orders of magnitude higher than the mathematical community’s standard of valid proofs."

[Joe Hendrix]

If that's actually true, then the problem of untrustworthy results in mathematics is much worse than I expected.

[Kevin Buzzard]

That's most definitely true, but to a large extent that's because getting Lean code to compile is very hard. I lecture the insolvability of the quintic to undergraduates but I think this is one of the questions on Freeks list that nobody did yet

[Kevin Buzzard]

.

[Kevin Buzzard]

But your conclusion is wrong because we're REALLY GOOD at knowing whether vague arguments can be formalised. That's the skill we're continually practicing by explaining maths to each other

[Kevin Buzzard]

We are really good at leaving out a large amount of details because we understand how maths works

[Kevin Buzzard]

But the process does involve a lot of trust...

[Joe Hendrix]

Ok, I think I see how Thurston was interpreting "standard of correctness and completeness". For me, it means did you actually think through why a particular program should work as intended on all cases, which often isn't true even for code in widely used software. Whereas I think his and your interpretation interprets it as meaning "did you specify the code or mathematical proof precisely". Getting a computer program to run requires a level of precision not found in mathematics, but as everybody knows that doesn't mean it is actually doing only what was intended.