Lessons from History

Stream: general

[Thomas Eckl]

When rereading Quinn's AMS article I realized that it does not contain a very extensive description of the "definition-and-proof technology" introduced around the turn of the last century, and why Quinn thinks it was (and is!) so successful with mathematicians. You find more in his (unpublished) book on https://intranet.math.vt.edu/people/fquinn/history_nature/nature0.pdf .

[Heather Macbeth]

Regarding the new logical foundations of the early 20th century, Quinn (in his AMS article linked by @Thomas Eckl in the earlier thread) suggests an interesting advantage of rigour:

this approach has unexpected advantages. Trying to fix gaps in first approximations to proofs can lead to conclusions we could not have imagined and would not have dared conjecture. They also make research more accessible: rank-and-file mathematicians can use the new methods confidently and effectively, while success with older methods was mostly limited to the elite.

[Thomas Eckl]

In his book, Quinn sketches a "science of contemporary mathematics" which aims to describe the practice of core mathematics where rigour plays an essential role, from many different angles: historical, sociological, pedagogical, philosophical, ... I particularly like the remarks using cognitive neuroscience which explain that mathematicians pack mathematical concepts into (equivalent) definitions, examples, first consequences because this allows them to build internal models of perception, as humans do for all sorts of perceptions. These models can be more or less useful, and that's why in the beginning theories are so fluid: mathematicians look for the right way to package them into the brain. In the relevant chapter Quinn extensively discusses an algebraic hierarchy - a hint why Lean is so successful with formalizing maths. (-;

[Thomas Eckl]

I find work like Quinn's so important, because they give clues how the next revolution in mathematics can and should be shaped. There is a revolution ahead, since the methods of 20th century mathematics come to their limit, as all the entertaining examples of published proofs of important results that are in doubt or right away false show. And proof assistants are there to help us out, but then better design them in a way that makes them fit successfully into the core mathematician's practice, and even makes it more effective. That's how it worked last time around.

[Johan Commelin]

Interesting thoughts! I would love to discuss this with you in more detail. But I should maybe first try to get my hands on that book by Quinn (-;

[Jalex Stark]

Quinn's (draft) book is freely available from quinn. Thomas linked it earlier.

[Johan Commelin]

Thanks, must have missed that other link

[Heather Macbeth]

In the last wave of formalization, more precise definitions led to famous counterexamples, which helped to convince mathematicians that these precise definitions were meaningful or necessary. Quinn mentions the nowhere-differentiable function and the space-filling curve (in his AMS article), which are well-known. In his book (section 9.2.1) he mentions a third example, about a definition I had not known was controversial at the time:

We now know that analytic techniques require a ‘smooth structure’ and not all manifolds have them. However early proposals to work with smooth structures were rejected on philosophical grounds: manifolds should be objects, not structures on an object. Furthermore, smooth structures seemed to amount to assuming what you wanted to prove, and seemed intellectually dishonest if not logically circular.

Apparently the modern definition of manifold was not fully accepted until Milnor's nonstandard smooth structures on the 7-sphere proved its necessity (in 1957!!).

Most mathematicians believe that there are a certain number of wrong theorems out there, but probably most mathematicians think we have found the right definitions. I wonder whether this wave of formalization will bring any wild counterexamples to change that consensus.

[Kevin Buzzard]

The Milnor fact is extraordinary. Grothendieck was defining schemes to be structures on topological spaces in the late 50s.

[Thomas Eckl]

Finding such counterexamples would be a strong case for formalization. However, the problem at Milnor's time was that it was not universally accepted to peel off layers of structures of well-known (geometric) objects. Now, where is the current conceptual framework whose formal specification would lead to new (counter)examples by analysing the finer details?

[Thomas Eckl]

My bets are on the new ways to "argue up to isomorphisms" developed in homotopy type theory, but you may have different suggestions ...