This is a longish essay by Gabe on his take on the history of mathematics.
He walks through how we made progress in mathematics in several eras, covering the methods by which we made this massive progress.
He ends with what we can learn from this and what other problems we apply these methods to.
Out of the essays Gabe has written, it is one of my (remember’s) favourite essays. I’ve included the intro and the eras of mathematics here, and highly recommend reading the rest of it.
This is a longish essay (~9K words). If you like computer science, you will likely enjoy reading it and will learn something.
But it is so much more than fun tidbits. This is the story of one of Humanity’s biggest triumphs, and I believe there is a lot to relearn from it.
I hope you will appreciate reading it.
Formalism is the view that maths and logic are primarily about syntax, what one can do within very precise rules of symbol manipulation. This is opposed to maths being about numbers, shapes, or a world of abstract ideas.
Formalism underpins our modern understanding of maths, logic and computer science. It is the core insight that led to the computing revolution and our modern understanding of scientific modelling.
Thanks to our now-formal understanding of logic, we built machines that can automatically check mathematical proofs for us. It’s interesting to reflect on how we got there.
—
Alas, I am not a maths historian.
Fortunately, I am a writer! I have a story of maths that I like to tell, and people like to hear it.
Its key points are all factual.
This is by no means the only story of maths one could tell. For instance, one could focus on social aspects, like the rise of scientific education. That story would connect math progress to the Golden Age of Athens, the Islamic Golden Age and the Age of the Enlightenment.
Nevertheless, my story is about formalism, and I don’t think I have ever seen the story of maths spelled out this way.
The Informal Era (–14th). People did maths that was mostly about numbers, and they did so in prose. It was painful.
The Notational Era (14th–19th). Mathematicians discovered and standardised notations. This led to an explosion in maths with many fields being created.
The Foundational Era (late 19th–1930s). Mathematicians, puzzled by the new heights they reached, sought to discover the nature of maths.
The Formalist Era (1930s–). To a large extent, they succeeded! We now consider their solution obvious, and have built most of our techno-scientific stack on top of it.
This is a major adventure, a big win for team Humanity.
We need more wins like this!
The final section lists a few learnings from this win, that we ought to apply to our own problems.
I think most working mathematicians would not agree that we are presently in the formalist era.
Many would state rather emphatically that they study a “Platonic realm” of math structures and would express their beliefs that those structures don’t have much to do with the linguistic and formal means used to study them, but exist objectively regardless of the “auxiliary” linguistic formalisms.
Others (e.g. V.I.Arnold) would emphasize the connections with physics and would actively promote the idea that excessive Bourbaki-style formalization is harmful.
Yet, we might be about to actually enter a formalist era with both humans and AI systems gradually becoming more and more fluent with automated formal theorem provers like Lean.
I think this is mostly a fish-in-the-water effect. The Platonic realm has little to do with Plato’s realm anymore. The Platonic realm is now that of syntax.
In the past, the epistemology of Platonic mathematics was that of the intuition (“I feel it”) or observation (“I see that literally all triangles obey the Pythagorean theorem”).
But now, however Platonist mathematicians may describe themselves, they take syntax is the de-facto source of truth.
If you have an intuition for a proof of a theorem or the existence of an object, and when you try to formalise it (even in a proof sketch, not necessarily Coq), you consistently fail, it’s strong evidence that the intuition was groundless. This is because we trust syntax much more than intuition or observation nowadays, which is what it means to live in the formalist era.
If an AI was to generate mechanistic counter-proofs of theorems that were “proven” in prose, regardless of how illegible the counter-proofs was, mathematicians would defer to it and not their intuition or the perception of the platonic object.
This is in stark opposition to the pre-formal times, where people routinely created paradoxes (think Zeno more than Russel) and faulty reasonings, even in the realm of maths.
I see this as just correct calibration: if tomorrow, someone developed a Platonistic telescope, that let us see the mathematical abstractions for what they are in the Platonic realm of ideas, in a way that we would trust more than formal proofs when both disagreed, then we would move on from the formalist era.
But the formalist era has this air of definitiveness, in that no mathematician expects to ever discover such a Platonistic telescope. In practice, we all defer to the syntactic rules, and intuition are just heuristics that sometimes let us go faster or bring us some nice intuitions, when they don’t lead us astray.
That does not correspond to my observations of the math community (or to my introspection as I have done some math research in my life and published some math papers).
On one hand, mathematicians tend to downgrade proofs which are impossible to intuitively understand. They would say, “ok, we now know that the statement is true, but any potential for better understanding of adjacent areas is not gained yet, or, perhaps, even lost, because people are not going to study this problem now, and so this achievement might even be detrimental to our field, as it is the interconnections between notions and subfields of study which truly matter the most, and they will not be discovered now, because the motivation to study this particular question is largely lost”. (In reality, of course, this would depend; some statements are so important and central, that it matters more that we know their status, than any gain from them motivating further research.)
I think most mathematicians think about themselves as having a “Platonistic telescope” inside their minds, although this “telescope” is imperfect, similarly to a physical telescope.
Here I can try to fall back onto my introspection. As a mathematician, I have mostly studied various partial orders with additional structure (“Scott domains” in their various incarnations, e.g. continuous or algebraic lattices, and such). I certainly think those objects actually exist “out there” in the “abstract realm”. An informal Hasse diagram does more to me than any syntactic description. So, although the field is trying to be algebraic (these structures are used as semantic domains in the field of denotational semantics of programming languages, and so can be useful in some approaches to formal proofs of software correctness), my intuition about them is mostly informal and geometric. In reality, I switch back and forth between those informal geometric ideas and syntactic aspects which I need when I focus on more low-level technical aspects (e.g. how to actually make a proof to go through).
I think you have misunderstood my point (and thus that I wasn’t clear enough).
Regardless of how they feel about non-intuitive proofs, when these proofs contradict their intuitions, the non-intuitive proofs will still be the source of truth.
They might feel bad about this stance, they might not identify with it, they might feel that this stance is sometimes detrimental. But it is the stance they enact. Belief in belief et al.
--
I think you are case in point of the “fish-in-water” effect that I am trying to describe.
You mention Hasse diagrams. They are a modern purely formal construct.
They are a convenient notation that is strictly equivalent to describing the elements of a partial ordered set in matrix form.
In the past, what you would have gotten is a lot of prose that may or may not have maintained the partial ordering properties, with some diagrams that would be much less clear.
Sometimes they would imply irreflexivity, sometimes not.
Sometimes they would imply more structure like a directed partial order, sometimes not.
Without any understanding of the implications.
You may want to think of non-standard models of arithmetics, where it wasn’t clear that First Order Peano arithmetic did not capture the integers. Or of Euclides’ axioms.
--
I think your mention of Scott domains is great!
So, as a student (not as a researcher), I actually got acquainted with DCPOs and Scott domains, specifically in the context of denotation semantics.
One of my teachers was actually quite interested in general (non-Haussdorf) manifolds.
I think this is precisely one of the realms where formalism shines.
I expect it would have been impossible for the field to take off without formalism.
There are so many broken intuitions in non-metric geometry! If we were left at the intuitions as being the ground truth, the field could not have succeeded. (Even in beginner metric geometry, it is easy to get screwed when one is not clearly introduced to specific examples where the definitions of closed/bounded/compact differ.)
There are just too many different types of spaces/topologies/manifolds, with different axioms behind them. The “true objects” here have little to do with standard numbers, intuitive euclidean spaces et al.
To the extent one has “true objects” in minds, these object are of a purely formal nature.
They have the shape of “these different formal systems are isomorphic in some sense” (you can encode the rules of one in the other, and get the same constructions as a result), and “I have some heuristics about these formal equivalence classes” (in the sense of an A-star heuristic).
The telescope that lets mathematicians check whether something is there or not is formalism, not their intuition.
Again, this is the practice that mathematicians have. As you said, when you start to prove, you check against the formal low-level. So de-facto, this is where you ground truth is.
I have met many mathematicians who were calibrated about this. They developed an internal calibro-meter that tells them how strong an intuitions is and in which rule systems they apply. And they transcend the feeling of the object existing, they just take intuitions as useful heuristics.
changing the order a bit:
That’s awesome! I’d love to understand more about manifolds in this context. We managed at some point to progress to reconciling Scott domains with linear algebra (with some implications for machine learning), but progressing to manifolds is something else.
Yes, absolutely. But only when one is engaging in the interplay between the formal and the informal.
The informal and the formal have to go together, at least when humans practice math.
The question is, what is formal. Are categories and toposes well defined? A follower of Brouwer and Heyting would tell you “no”.
And can one work with the objects before their formalization is fully elucidated? One often has to, otherwise one would often be unable to obtain that formalization.
When one is talking about the cutting edge math, math which is in the process of being created, the full formalization is often unavailable, yet progress needs to be made.
back to the beginning:
Yes, absolutely, but it will be a very incomplete truth.
The intuition about what is connected to what is an important part of the actual mathematical material even if that intuition is not fully reified into definitions, axioms, and theorems.
So yes, this is a valid source of mathematical truth, but all kinds of informal considerations also form important mathematical material and empower people’s ability to obtain the formalized part of truth as well. E.g. if one looks at the Langlands program, one is clearly seeing how much the informal part dominates and leads, and how the technical part gradually follows, conjectures evolving and changing before they become theorems.
From the simple example of my own studies, if one wants to obtain generalized metrization of Scott topology, this task is obviously very informal. Who knows what this generalized metrization might be a priori… All one understands at the beginning is that ordinary metrics would not do because the topology is non-Hausdorff. Then one needs to search, and one first finds that the literature contains the “George Washington bridge distance” quasi-metrics, where an asymmetric distance is non-zero in one direction and zero in the opposite direction, just like the toll on that bridge. And then one proves that a topologically correct generalized metrization can be obtained this way, but when one is also trying to figure out how to compute this generalized distance, one encounters obstacles. And then one realizes that the axiom d(x,x)=0 is incompatible with distance being monotonic with respect to both variables, and, therefore, is incompatible with distance being Scott continuous with respect to both variables, and Scott continuity is the abstract version of computability in this field. And then one proceeds to (re)discover generalized metrics which don’t have the d(x,x)=0 axiom obtaining (symmetric) relaxed metrics and partial metrics which can be made Scott continuous with respect to both variables and can be made computable, and so on.
The informal part always leads, formalization can’t be fruitful without it (although perhaps different kinds of minds which are not like minds of human mathematicians could fruitfully operate in an entirely formal universe, who knows).
Only if the set is finite.
If one wants to represent an infinite partially ordered set in this fashion, one has to use an informal “Hasse-like sketch” which is not well-defined (as far as I know, although I would be super-curious if one could extend the formal construct of Hasse diagrams to those cases).
I am going to link to a few of the examples of these informal Hasse diagrams. I am going to use this text originally from 2002 (and the diagrams are all from 1990-s): https://arxiv.org/abs/1512.03868
On page 15 (page 30 of the PDF file), we see an informal “Hasse diagram” for interval numbers within a segment. On page 16 (page 31 of the PDF file), this “Hasse diagram” is used in an even more informal fashion (with dashed lines to indicate that these lines are not a part of the depicted upper set Va,b).
On page 103 (page 118 of the PDF file), we see a more discrete infinite partial order, yet even this more discrete case is, I believe, beyond the power of formalized “Hasse diagrams” (it’s not an accident that most elements have to be omitted and replaced by ellipsis-like dots looking like small letters “o”).
I think this is more the start of a pleasant long discussion over beers (or tea/coffee) than of a thread that would take a lot of time to write, and that very few people would be interested in.
Feel free to DM me on Twitter (I am more responsive there) if you are ever in Europe, I think it would be fun!
But very quickly, to not leave you pending:
I agree, and I think that they work as pointer for people who already know the corresponding formalisations and their limitations.
If used in other situations, I expect they largely do not work. Concretely, I expect that readers/students/attendees will reliably come out with wrong intuitions, and that proofs with tend to include mistakes.
I have seen “intuitive” diagrams hiding mistakes so many times, both in ML and in type theory. Whether they represent proof derivations with holes, neural network architectures with holes, calculations with holes, infinite graphs with holes, etc. The infamous “x1 + x2 + … + xn” that is not always well defined.
Yup, I was going to say something similar.
I believe this is more an artefact of how we humans operate than of the truth of things.
For instance, I believe that it is possible to write an automated theorem prover that proves most of the theorem pre-15th century, and that it is impossible for people pre-15th century to prove most of the things that this automated theorem prover could prove.
In practice, we humans are quite biased towards positing the existence of entities behind any perceived regularity. (Spirits, phlogiston, ethers, new-age energies, etc.)
Usually, these entities do not exist, and there was no coherent deep generalisation behind the regularity.
Sometimes, the regularities are not even there, and we just hallucinated them.
I think maths is roughly similar. That there are things, but that said things are not Plato’s squares and standard numbers, but just equivalence classes of symbolic manipulations. We may perceive regularities through our intuition, and sometimes have intuitions precise enough to be useful, but it’s all downstream of that source of truth.
Thanks!
I will certainly grant you the main point: we see tons of errors, even in the texts written by leading mathematicians. There is still plenty of uncertainty about validity of some core results.
But that’s precisely why it is premature to say that we have entered the formalist era. When people start routinely verifying in automated theorem provers, that’s when we’ll be able to say that we are in the formalist era.
I am not an expert, but it seems to me that you still need some kind of intuition to guide you, considering that it is impossible to define even such seemingly simple ideas like “natural number” in first-order logic.
Machine proofs are a great thing, but without interpretation, we wouldn’t know what they are actually about. Like, the machine can show that if you have axiom X, Y, Z, you can prove Q. Sure, but what do those axioms mean, and why should I care about them? (I mean, I could just generate random axioms, and let the machine find some statements that can be proved from them, but would anyone want to read that?)
Hmmm… I don’t think this accurately describes the era of mathematics starting around the 1920s. In fact, I would argue that the correct era would be about 1910-1937, starting with Russell and Whitehead’s Principia Mathematica and ending with the proof that the lambda calculus is exactly as powerful as the Turing machine.
This era was focused on applying logic to computation. It saw the development of type theory and the foundations of computation. Some aspects, like the halting problem, were related to logical consistency, but I think the more important breakthroughs had to do with formalizing computation.