It really is remarkable. I think the most remarkable fact about it is that the intensional identity type was invented by Martin Lof in the 70s, the groupoid model was discovered in the 90s and then finally in the late 2000s various people made the connection that Martin Lof's original system from the 70s was in a sense already a type theory for abstract homotopy theory. This led to an explosion of new ideas in type theory (univalence, higher inductive types, modalities) that took a somewhat obscure field of math/cs to the thriving research community it is today.
I’ll admit to coming late to the party (when a friend introduced me in 2013), but what’s amazing to me is when you take the step of encoding your cellular structures as adjacency matrices.
You can visually see structures of your theory (eg, facts about groups) in the patterns of terms in the matrix.
Eg, diagramming a cyclic group ends up with a banding pattern in the portion of your matrix denoting equivalent pairs under the operation… which shows that in some sense, the level maps of + on Zn x Zn form a twisted torus. (Which makes sense in hindsight, as you have the product of two loops with the level maps wrapping around non-trivially.)
That you get ideas such as that by chasing through a purely abstract definition (groups -> diagrams) is wild to me.
Edit:
I actually built a simple case (Z4) in Minecraft — just because I found it surprising.
> How can roots be changed without a redo of the universe?
This is a very interesting question and I think reflects a mismatch between how we commonly think about of foundations of mathematics and what role foundations actually play in mathematics. There's no recording online but I recommend looking at the slides to Mike Shulman's talk from JMM 2022 where he discusses this point: http://sigmaa.maa.org/pom/Slides/shulman-2022jmm.pdf . Mike works on, among other things, homotopy type theory, the subject of the original article.
His basic point is that we should think of math more like programs that we can "compile" to various backends. If your math is high level it's not necessarily tied to a particular "architecture" like ZFC.
> Math isn’t empirical: it’s assumed axioms which define a formal system.
There are mathematicians who would disagree. They would say that math is discovered, not invented and that axioms don't actually matter. They would also say that mathematicians may study axioms using mathematical methods but need not base their methods on axioms or formal systems. They would say that you can switch out your foundations and have the same math for all purposes you care about (if you don't care about axioms).
While I don't agree with everything there, I think they definitely make a point that's worth thinking about. For example, very few mathematicians would be able to spell out from memory "their basic axioms" (maybe ZFC, category theory, etc., maybe they don't even know or care, or switch depending on context). Now why is that? Their work is so far removed from foundations that they don't have to care. They will rightfully demand that their theorems and ways of reasoning be supported by the axioms. Beyond that, you can tinker and change them all you please. They only need a small part of your foundations to do their work. Crucially, most of them wouldn't "waste" their precious time on e.g. "formalizing that minimal foundation".
Maybe one could view foundations as a bunch of programming languages where using the high level features looks indistinguishable and almost noone uses the low-level. I think this intuition strongly suggests that eventually computers will win and all mathematicians will use proof systems (maybe without even knowing how they work under the hood). That is, until maybe the machines surpass their reasoning ability so much that humans are obsolete in that space.
empirical mathematics will never subsume all of mathematics, unless we have AGI then a strong maybe. This goes back to Plato at least, who said incommensurability is not something the physical senses could ever know. Physical lengths with no common unit measure will never be found empirically, as the instruments will first be assumed to not be precise enough.
There’s no round about way through empirical means to incommensurability. Some wider-than-empiricism epistemology must be incorporated because of this one example.
The empirical/constructive? mathematicians are right to differentiate their method. But their method is unable to handle some math. And that’s fine.
I think this extends to computers. The Halting problem is too similar to empirical ulimitations. Now maybe some kind of AGI that is smarter than humans could one day peer into this non-emprical mathematical world much better than us. But will we be able to confidently trust everything it claims? Will we run empirical tests on it to make sure it’s functioning correctly and therefore trust it’s conclusions? Maybe. It’s kind of hard to say right?
Mathematicians who thought that way are what led to formalisms:
They couldn’t agree on if continuity implied the existence of a derivative, necessitating the need for formal models and reasoning.
Most software engineers don’t care about compiled assembly (and their work can be compiled to many flavors), yet it’s accurate to describe their work as creating streams of assembly instructions which can be automatically executed by a cleverly designed piece of silicon.
The goal of formalisms has always been precisely what you say: a low-level backend that supports the high-level abstractions of working mathematicians. But just as with computers, it’s worth understanding “the stack” to appreciate what mathematics is.
Math works on tons of things that don't exist. Physics uses math because it seems to work (most) of the time. The assumption that the universe works mathematically is just an assumption that hasn't failed catastrophically yet.
By itself Metamath doesn't embed any particular set of axioms. The most widely used database (axioms and proven theorems) uses classical logic and set theory, but there's also databases for intuitionistic set theory, new foundations, and higher order logic.
Great read, I was expecting it to bring up the four color theorem, but it was actually an even more interesting debate touching on some modern mathematics.
I think it's still worth bringing it up: https://en.m.wikipedia.org/wiki/Four_color_theorem In a nutshell, they proved that all maps of contiguous countries can be colored using only four colors by reducing the infinite set of possible maps to a finite one and then having a computer check each case. In the 70's, this wasn't considered a 'real' proof, and it was argued that we can't trust the machine the way we can trust human mathematicians. My first reaction upon hearing about that debate was similar to what probably most HN readers would think, that it's arguably the other way round and we should ideally only trust proofs that had been fully formalized by machines. Glad to see that we're making progress in this direction.
Also worth mentioning: apart from Coq that was discussed in the article, there's also the Lean theorem prover that also features some more general programming elements, it's regularly discussed on HN:
> In the 70's, this wasn't considered a 'real' proof.
I ran into that decades ago. We used the original Boyer-Moore theorem prover [1] as part of a program verification system. The system had two provers, the Nelson-Oppen simplifier (the first SAT solver) to automatically handle the easy proofs, and the Boyer-Moore system for the hard ones. To make sure that both had consistent theories, I used the Boyer-Moore prover to prove the "axioms" of the Nelson-Oppen system, especially what are usually called McCarthy's axioms (the ones that use Select and Store) for arrays.
The Boyer-Moore system uses a strictly constructive approach to mathematics. It starts from something like Peano arithmetic (there is a number zero, and an operation add 1) and builds up number theory. So I added a concept of arrays, represented as (index, value) tuples in sorted order, and was able to prove the usual "axioms" for arrays as theorems.
The machine proofs were long and involved much case analysis.[2] I submitted a paper to JACM in the early 1980s and got back reviews saying that it was just too long and inelegant to be at the fundamentals of computer science. That might not be the case today.
A few years back, I put the Boyer-Moore prover on Github, after getting it to work with Gnu Common LISP. So you can still run all this 1980s stuff. It's much faster today. It took about 45 minutes to grind through these proofs on a VAX 11/780 in the early 1980s. Now it takes about a second.
The proof log [2] is amusing. It's building up number theory from a very low level, starting by proving that X + 0 = X. Each theorem proved can be used as a lemma by later theorems, so you guide the process by giving it problems to solve in the right order. By line 1900, it's proving that multiplication distributes over addition. Array theory, the new stuff, starts around line 2994.
The reason this is so complicated and ugly is that there's no use of axiomatic set theory. Arrays are easy if you have sets. But there are no sets here. Sets don't fit well into this strict constructive theory, because EQUAL means identical. You can't create weaker definitions of equality which say that two sets are equal if they contain the same elements regardless of order, because that introduces a risk of unsoundness. Effort must be put into keeping the tuples of the array representation in ascending order by subscript, which implies much case analysis. Mathematicians hate case analysis. Computers are good at it.
If you have to rely on the computer to validate a proof you then have to rely on the whole supply chain that generated the computer as well as the software for the proof checker. Proofs need to be dense enough that we can discover them in a long lost tomb and eventually figure out what that collapsed civilization had learned.
> If you have to rely on the computer to validate a proof you then have to rely on the whole supply chain that generated the computer as well as the software for the proof checker.
This is true, but a similar problem plagues typical proofs.
> Proofs need to be dense enough that we can discover them in a long lost tomb and eventually figure out what that collapsed civilization had learned.
This is almost never the case for modern mathematical research. Case in point, some of my current work relies on the classification of finite simple groups. Therefore, in practice, it is impossible to validate my results from first principles.
Why does that classification preclude validation? Is that classification not imposed as part of your proof? I guess what I'm not so seriously wondering is what is the point of it, if it can't be understood without relying on a stupidly complex network?
Yes, but you only need one machine for all proofs (that its internal logic can represent), so all the efforts towards removing flaws from that system benefit all proofs, whereas classic review only ever benefits a particular proof (and other theorems that build on it). It just scales better. And that's probably what's needed to keep up with the pace of modern research. It's not unheard of for proofs to be citing theorems that were only published on arxiv. It's not even unheard of for proofs that were published in reputable journals to be retracted because errors were discovered later:
Prof. Byron Cook (pure math at UCL) is arguably a driving force behind a lot of the recent adoption of theorem provers. He's talked a lot about those problems (in fact, I was partially paraphrasing him from memory above). You can read up on what he said directly, I found it pretty convincing that proof verification is where modern mathematics should be moving towards (and probably will, there are collaborative efforts to re-prove substantial parts of modern mathematics using automated provers).
Btw, do you have any support for your claim that proofs must be dense enough to fit onto a tombstone? I've literally never heard that before, and by your definition, pretty much no recent mathematical research would qualify. We've come a long way since Euclid.
What's the size of a tomb? Is there some kind of symbol limit? Modern proofs easily run into the hundreds of pages, is that too long? And do you have any support for those requirements, or is that just your personal conviction?
You are limited to 100 cubits cubes and must include all sources fully expanded on high quality papyrus scrolls. I have high quality sources for my personal convictions unfortunately I cannot provide them in this medium for they are on high quality papyrus.
> “The drive to mechanize proof and proof verification doesn’t strongly motivate most mathematicians as far as I can tell,” he [Michael Harris] said. “I can understand why computer scientists and logicians would be excited, but I think mathematicians are looking for something else.”
I'm not a mathematician, but I have at times been able to consider myself a computer scientist. To me, the goal of "mechanizing" and formalizing mathematics seems instinctively recognizable as a worthwhile pursuit, for the same reason it's worth adding tests to an unwieldy legacy codebase: it makes it possible to refactor, to experiment and break things and see what happens.
The more we formalize the most fundamental axioms and theorems of mathematics, the more confidently we can alter or remove them and see what happens to the rest of the system. Achieving "100% test coverage" and "instrumentation" of mathematics would allow us to analyze the system under stress. We could fuzz it. We could refactor it. We could even ask an AI to do that for us.
As a relative layman, I'm often struck by how many mathematical theorems are dependent on the arbitrary paths we took to develop them. For the same reason, it's a common occurrence that one mathematician discovers an innovation in one branch of mathematics by simply borrowing a common technique from a distantly related branch. Those sorts of analogies and connections between ideas are difficult for humans to spot, and their discovery scales linearly with the number of mathematicians, who might prefer to spend their time discovering truly new ideas rather than repurposing those already existing ideas.
But computers, on the other hand, are excellent at spotting these relationships, if given sufficiently formalized definitions of them. So that's why I'd be most excited about formalizing mathematics: how much low-hanging fruit is waiting to be discovered by computers that are just missing the right prompt?
Most mathematicians aren't interested in refactoring their mathematical "codebase", nor experimenting with axioms. They simply want to understand and discover more math. The reasons you state for your interest in formalisation don't appeal to most mathematicians.
Concerning analogies and borrowing techniques between fields, this is absolutely something humans are good at and which it is very hard for computers to do. Why do you think otherwise? To take a very simple example, most mathematical objects can be represented in different ways. A mathematician can fluently move between these representations, whereas computers cannot. This is a largely the obstacle for the adoption of proof assistants among mathematicians.
Well, as a computer scientist, I'd urge them to reconsider. :) My intuition is that, given a sufficiently formalized system, computers can help them achieve their goal of understanding and discovering more math, much more rapidly and with compounding effects. Although perhaps there is a risk that any mathematics the computer might "discover" would become increasingly incomprehensible to human mathematicians, in which case the discoveries wouldn't be worth much.
I agree that humans are better at borrowing techniques between fields, but we can't do it quickly, and we can't systematically mine the entire "codebase" for these relationships (hence why "discoveries" in 2020 can combine ideas from 1990 and 2000). Besides, I suspect much of that gap between human and computer ability is due to a lack of a properly formalized representation of the ideas within each possibly related field. To use a programming term, it's a "code smell" if we haven't properly encoded the relationships between two fields. Sure, we can manually identify them, and then build on them once we do. But why did we need to bother in the first place? Wouldn't a formal system have made the relationships obvious, or at least more automatically discoverable?
Large language models have also changed my view of what computers are capable of, and in that context I've been most impressed with their ability to analogize and explain relationships between seemingly arbitrary sets of ideas. It makes sense they'd be good at this, since the premise of training them is to construct a web of weights that's indecipherable to humans but fundamentally enabling to the language model. Stephen Wolfram has been writing about how language models seem to encode a certain "truth" which has always existed but which we've never recognized. This idea resonates with me and I expect models have a lot to teach us about our own consciousness and how we model the world.
But on the other hand, if LLMs are so successful, by definition, at identifying relationships without being given formal representations of them, then why bother formalizing mathematics? After all, mathematics only exists because we can communicate its ideas by constructing the language of mathematics as a sort of amalgam of spoken language and abstractions we create within it. And while the exercise of formalizing the relationships between those abstractions might identify some imprecisions or mistaken assumptions in the existing hybrid of spoken language and formalized chunks of math, do we really need to bother? For an advanced LLM, shouldn't our existing definitions become naturally encoded into its weights during training, so that any emergent formalisms can be poked and prodded when we talk to it or ask it to reason about them? Or will it get stuck on the same imprecisions that we might identify when trying to manually formalize our existing systems of mathematics?
I don't quite understand what you are saying about llms. Language models are sort of a reverse engineering of the ways humans learn. I imagine if you read basically the whole internet and meaningfully memorized it you would be able to connect a bunch of dots too. Computers are just fast. Math viewed as tool doesn't require formalization, math as an endevour does. Sometimes exploring a theory is useful sometimes it's only interesting in itself
Asking working mathematicians to formalize their proofs in a machine-checkable system is like asking photographers to become electronics engineers so they can build their own digital cameras from scratch. It's not a reasonable request. It's so far outside of a typical mathematician's lane it's not even on the same continent.
They could do what every other scientist does, and pay people to build and run the tools they need to get scientifically valid results from their experiments.
Math isn’t science. Most mathematicians aren’t interested in applications to the real world. They don’t care about empiricism or validity. The fact that a lot of applications have come out of math is a side effect.
Imagine if someone discovered a way to solve real world problems by formulating them as chess positions. Would it be reasonable of us to demand that chess players stop competing and work on these formulations? No, and I don’t think many chess players would jump at the opportunity. They just want to play chess!
> Most mathematicians aren't interested in refactoring their mathematical "codebase", nor experimenting with axioms. They simply want to understand and discover more math.
Experimenting with axioms is one way you discover more math. For example, set theory: there’s a lot of math assuming ZF(C), but even more if you start looking at alternatives to it (like NBG, NF(U), constructive set theories, non-well-founded set theories, paraconsistent set theories, etc)
You're not wrong, but most mathematicians aren't working on (or even interested in) foundations. Not saying what you mentioned isn't math (I think it is), but my point still stands.
I am a mathematician and would love to mechanize my proofs. The issue is that systems like Coq construct proofs in a radically different way than how we were trained. I've struggled with Coq even with a somewhat more than a passing knowledge of the system; I used Coq's underlying language Gallina to write interpreters, which were then processed into OCaml while studying in graduate school. At the same time, I can barely turn out a basic proof in Coq.
What would help dramatically for me and others that work in applied math are proofs that cover the material in something like Principles of Mathematical Analysis by Walter Rudin. These are proofs that cover basic real analysis and topics like continuity, differentiation, and integration. It would also help to see basic linear algebra proofs such as that all real symmetric matrices have a real eigendecomposition. Now, these may exist and it's been a couple of years since I've looked. If anyone has a link to them, I'd be extraordinary grateful.
For the math that you mention, I would suggest looking at mathlib (https://github.com/leanprover-community/mathlib). I agree that the foundations of Coq are somewhat distanced from the foundations most mathematicians are trained in. Lean/mathlib might be a bit more familiar, not sure. That said, I don't see any obstacles to developing classical real analysis or linear algebra in Coq, once you've gotten used to writing proofs in it.
Thanks for sending by the mathlib examples. They're not particularly intelligible for me, but it's something to work towards.
Generally speaking, I work in the intersection between optimization, differential equations, and control. To that end, there's a variety of foundational results in things like optimization theory that I'd like to see formalized such as optimality conditions, convergence guarantees, and convergence rates.
Two questions if you know. One, which theorem prover would you recommend for working toward these kinds of results? Two, is there appetite or a place to publish older, known theorems that have been reworked and validated? And, to be clear, two is not particularly important for me and my career, but it is for many of my colleagues and I'm not sure what to tell them about it.
You're welcome! And likewise, thanks for the interesting reply.
I'm afraid I have no knowledge of your field, and no idea whether there are good tools and libraries for formalising the things you want. Maybe ask or have a look around the Proof Assistants StackExchange[1]?
There are many CS conferences through which you can publish formalised mathematics. One that comes to mind is ITP[2], but there are lots which are announced on mailing lists like TYPES-announce, coq-club, agda... You could look through previous versions of ITP and check out a few of the papers on formalising mathematics to get a feel for what these publications look like.
I am nothing more than an enthusiastic dabbler, but these have helped me.
There are two very different directions
1. the sort of full on proof automation with tactics https://direct.mit.edu/books/oa-monograph/4021/Certified-Pro... Dr. Chlipala builds up understanding of the "crush" tactic, which more or less lets you specify an inductive hypothesis, and that tactic fiddles around with identifying the base case, and expanding enough to generate the n+1 step. Along the way, you get exposure to using Gallina to write your own tactics.
it's neat, from a programmer point of view, because you can automate away the boring parts. There is pretty good discussion of debugging tactics, which might provide a path to transforming machine proofs into something a bit more comprehensible. at the very least, you can recover the application of axioms and such that did the transformation.
The other direction, that has been much more enlightening for me (the amateur hobbyist) was agda and Jesper Cockx's tutorial- https://github.com/jespercockx/agda-lecture-notes/blob/maste...
he builds up all of the notation from, well, nothing.
for example, you get refl, and then build up
-- symmetry of equality
sym : {A : Set} {x y : A} → x ≡ y → y ≡ x sym refl = refl
-- transitivity of equality
trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z (54) trans refl refl = refl
-- congruence of equality
cong : {A B : Set} {x y : A} → (f : A → B) → x ≡ y → f x ≡ f y cong f refl = refl
along with the syntax that comes with the agda std lib.
agda is different, but you can still extract to Haskell (and allegedly javascript for node, but that was a little flakey for me and might go away in a future release). less useful for your goals, much more programming oriented - https://plfa.github.io is pretty good, and worth mentioning as a reference.
Is the problem that human mathematicians have decided that classical logic + ZF(C) is the best framework for them–but it isn’t the best framework for computers?
Which raises an interesting philosophical question - do contemporary mathematicians mostly do things one way rather than another (i.e. classical logic instead of intuitionistic/paraconsistent/etc logic, ZF(C) set theory instead of alternative set theories or type theory or whatever, classical analysis instead of non-standard analysis, and so on) - because they’ve settled upon the inherently superior (easier, more productive) way of doing things - or is that just an accident of history? Could it be that in some alternative timeline or parallel universe out there, mathematics took some different forks in the road, and the mathematical mainstream ended up looking very different from how it does here?
I find these "fork in the road" questions endlessly fascinating, and that's exactly what I was getting at with my comment about the motivation for formalizing mathematics. And it doesn't just apply to math, but the whole "tech tree" of human history. How many seemingly arbitrary choices led us down a path that unknowingly diverged from some alternative future?
Last time I commented about this [0], I made some guy irrationally angry as he told me I sounded like I was 19 years old. And in an earlier comment [1], another guy took extreme offense to my questioning of the statement "with enough marbles, the discrete distribution behaves like a continuous distribution."
It seems there is some high priesthood of mathematics and physics that doesn't like when you ask these sorts of questions.
> Last time I commented about this [0], I made some guy irrationally angry as he told me I sounded like I was 19 years old
If people make comments like that, flag them and email dang (hn@ycombinator.com) and he’ll do something about them
> It seems there is some high priesthood of mathematics and physics that doesn't like when you ask these sorts of questions
In my personal experience, most professional mathematicians and physicists are open to questioning the foundations of their discipline, and deal charitably with doubters (even those who are coming from a place of misunderstanding).
I suspect most of the “high priests” you speak of aren’t actually professionals at all, just Internet randoms who (at best) know only slightly more than you do, and who know very little about the norms of civil dialogue
I can't speak for kxyvr, but let me chime in as a mathematician who does formalise my theorems. There's no issue with representing various foundations (e.g. ZFC) on a computer -- for example, that's essentially what Lean/mathlib does, and it's working out great for them. A "problem" with ZFC, however, is that it's very low-level, meaning there's a large distance between the "informal" proofs which mathematicians carry out and communicate, and their corresponding formal proofs in ZFC. Accordingly, for a ZFC-based mathematician to start using proof assistants, they not only have to learn how to use a proof assistant, but also to translate (or expand/elaborate) their math into ZFC.
In other foundations, such as homotopy type theory (which is what the article is about), the distance between "informal" mathematical arguments and their formal counterparts is much shorter. This is why formalisation is widespread in the HoTT-community. Indeed, I believe Voevodsky worked on HoTT in order to have a foundation which was much closer to the mathematical practice in homotopy theory.
Mechanized proofs ensure the correctness of the results they prove. That's useful. Indeed, the point of the article was that Voevodsky sought out proof assistants in order to ensure his math was correct.
As for your other questions: No, formal proofs are not intelligible to the average mathematician. They do not on their own grant insights, but the process of formalising a proof does often yield insights. (I speak from experience.) Not sure what you mean by "better"; they certainly don't replace ("informal") mathematical proofs.
The formalized proofs are useful because they allow you to formalize more difficult proofs. That's circular but let me explain. Formalizing all of mathematics in a formal, computer verifiable language is theoretically easy. The problem is that you don't want it to take forever to write down a proof because you have to go axiom by axiom. This is a problem of abstraction. Just like we need programming languages which have powerful, high level methods of abstraction, like functions, we need a formal language for mathematics that makes it easy to formalize proofs. You don't want to work with the axioms all the time, but instead use your oreviously proven results. When you have a good setup like this, writing down a proof formally should only take O(n) time, meaning it only takes up to some constant longer than writing down the informal proof. The goal right now is to get this constant down so it becomes appealing for the average mathematician to formalize their proof, without needing deep knowledge of type theory. This is happening right now with the Mathlib of Lean, a database of already formalized theory.
So where does this lead? As you build a large database of formalized mathematics you get some snowball effects. We can train language models just like on code to assist us. Formalizing natural language mathematics should merely be a process of translation, if set up correctly, not somwthing computationally advanced. Copilot for formal maths will being the constant lower. As correctness of formal proofs can be automatically checked, at some point you can let the system attempt formalizing Pdf documents by itself. This yields you a larger database, more traininf data etc. In 20 years I hope that we have a database of most.mathematics formalized in Lean, and language models that can translate between natural language math and Lean quite fluently. As any formal language of mathematics is also a programming language, we van start doing some very serious program correctness validation. You will not just run your Euler iteration until it has sufficiently small error, but you will instead run it up to your PROVEN desired error. Because we did all the work of formalizing mathematics, this will not be much harder than just writing the program normally. Mathematicians can also now work with these systems and thereby work quicker, saving time on reviews. Computer verified proofs will.not be unreadable, the database will be open source and constantly refactored and kept clean. Etc. Etc.
Well my whole point is that you have to build up a large codebase of formalized mathematics first, and you have to do it in an elegant way so it is easy to work with. Then verified programs is something we can start to realistically consider. But of course we can't do that yet (except in certain situations with great effort). It's really very similar to building up a whole software architecture. 30 years ago we were at machine code, now we are at maybe C. We want to get to the Figma of formalized mathematics. It will take many years but I don't see and conceptual hurdle, especially given the power of LLMs now.
All of these are open to contributions, and there are lots of useful basic things that haven't been done and which I think would make excellent semester projects for a cs/math undergrad (for example).
Odd choice of article title. It appears to be about the well known field: "foundations of mathematics", and is even in a section of the web site named "foundations of mathematics". Meanwhile the word "root" doesn't appear anywhere in the article.
58 comments
[ 2.4 ms ] story [ 86.9 ms ] threadThe topology of (category) diagrams can represent a type theory’s semantics — and equivalence in your theory is a question about paths in diagrams.
An application of the idea that topology connects “algebra” (type theory) to “geometry” (diagrams composed of cells).
You can visually see structures of your theory (eg, facts about groups) in the patterns of terms in the matrix.
Eg, diagramming a cyclic group ends up with a banding pattern in the portion of your matrix denoting equivalent pairs under the operation… which shows that in some sense, the level maps of + on Zn x Zn form a twisted torus. (Which makes sense in hindsight, as you have the product of two loops with the level maps wrapping around non-trivially.)
That you get ideas such as that by chasing through a purely abstract definition (groups -> diagrams) is wild to me.
Edit:
I actually built a simple case (Z4) in Minecraft — just because I found it surprising.
https://zmichaelgehlke.com/images/z4-plus-map.png
And you get all kinds of weird visuals in diagrams. Like “log” or “exponential” curves trying to diagram a whole field. (Z5, in this case.)
https://zmichaelgehlke.com/images/5-finite-field.png
This is a very interesting question and I think reflects a mismatch between how we commonly think about of foundations of mathematics and what role foundations actually play in mathematics. There's no recording online but I recommend looking at the slides to Mike Shulman's talk from JMM 2022 where he discusses this point: http://sigmaa.maa.org/pom/Slides/shulman-2022jmm.pdf . Mike works on, among other things, homotopy type theory, the subject of the original article.
His basic point is that we should think of math more like programs that we can "compile" to various backends. If your math is high level it's not necessarily tied to a particular "architecture" like ZFC.
One way to do that is set theory. Another is category theory. A third way is type theory.
We try to pick a set of assumptions that allow us to use the language to reason about the world around us — a modern ontology.
But is the Banach-Tarski paradox a fact about the real world? — or merely a part of the game we play? Hard to know.
https://en.wikipedia.org/wiki/Banach–Tarski_paradox
There are mathematicians who would disagree. They would say that math is discovered, not invented and that axioms don't actually matter. They would also say that mathematicians may study axioms using mathematical methods but need not base their methods on axioms or formal systems. They would say that you can switch out your foundations and have the same math for all purposes you care about (if you don't care about axioms).
While I don't agree with everything there, I think they definitely make a point that's worth thinking about. For example, very few mathematicians would be able to spell out from memory "their basic axioms" (maybe ZFC, category theory, etc., maybe they don't even know or care, or switch depending on context). Now why is that? Their work is so far removed from foundations that they don't have to care. They will rightfully demand that their theorems and ways of reasoning be supported by the axioms. Beyond that, you can tinker and change them all you please. They only need a small part of your foundations to do their work. Crucially, most of them wouldn't "waste" their precious time on e.g. "formalizing that minimal foundation".
Maybe one could view foundations as a bunch of programming languages where using the high level features looks indistinguishable and almost noone uses the low-level. I think this intuition strongly suggests that eventually computers will win and all mathematicians will use proof systems (maybe without even knowing how they work under the hood). That is, until maybe the machines surpass their reasoning ability so much that humans are obsolete in that space.
There’s no round about way through empirical means to incommensurability. Some wider-than-empiricism epistemology must be incorporated because of this one example.
The empirical/constructive? mathematicians are right to differentiate their method. But their method is unable to handle some math. And that’s fine.
I think this extends to computers. The Halting problem is too similar to empirical ulimitations. Now maybe some kind of AGI that is smarter than humans could one day peer into this non-emprical mathematical world much better than us. But will we be able to confidently trust everything it claims? Will we run empirical tests on it to make sure it’s functioning correctly and therefore trust it’s conclusions? Maybe. It’s kind of hard to say right?
They couldn’t agree on if continuity implied the existence of a derivative, necessitating the need for formal models and reasoning.
Most software engineers don’t care about compiled assembly (and their work can be compiled to many flavors), yet it’s accurate to describe their work as creating streams of assembly instructions which can be automatically executed by a cleverly designed piece of silicon.
The goal of formalisms has always been precisely what you say: a low-level backend that supports the high-level abstractions of working mathematicians. But just as with computers, it’s worth understanding “the stack” to appreciate what mathematics is.
By itself Metamath doesn't embed any particular set of axioms. The most widely used database (axioms and proven theorems) uses classical logic and set theory, but there's also databases for intuitionistic set theory, new foundations, and higher order logic.
I think it's still worth bringing it up: https://en.m.wikipedia.org/wiki/Four_color_theorem In a nutshell, they proved that all maps of contiguous countries can be colored using only four colors by reducing the infinite set of possible maps to a finite one and then having a computer check each case. In the 70's, this wasn't considered a 'real' proof, and it was argued that we can't trust the machine the way we can trust human mathematicians. My first reaction upon hearing about that debate was similar to what probably most HN readers would think, that it's arguably the other way round and we should ideally only trust proofs that had been fully formalized by machines. Glad to see that we're making progress in this direction.
Also worth mentioning: apart from Coq that was discussed in the article, there's also the Lean theorem prover that also features some more general programming elements, it's regularly discussed on HN:
https://news.ycombinator.com/item?id=36107796
https://news.ycombinator.com/item?id=34456573
I ran into that decades ago. We used the original Boyer-Moore theorem prover [1] as part of a program verification system. The system had two provers, the Nelson-Oppen simplifier (the first SAT solver) to automatically handle the easy proofs, and the Boyer-Moore system for the hard ones. To make sure that both had consistent theories, I used the Boyer-Moore prover to prove the "axioms" of the Nelson-Oppen system, especially what are usually called McCarthy's axioms (the ones that use Select and Store) for arrays.
The Boyer-Moore system uses a strictly constructive approach to mathematics. It starts from something like Peano arithmetic (there is a number zero, and an operation add 1) and builds up number theory. So I added a concept of arrays, represented as (index, value) tuples in sorted order, and was able to prove the usual "axioms" for arrays as theorems.
The machine proofs were long and involved much case analysis.[2] I submitted a paper to JACM in the early 1980s and got back reviews saying that it was just too long and inelegant to be at the fundamentals of computer science. That might not be the case today.
A few years back, I put the Boyer-Moore prover on Github, after getting it to work with Gnu Common LISP. So you can still run all this 1980s stuff. It's much faster today. It took about 45 minutes to grind through these proofs on a VAX 11/780 in the early 1980s. Now it takes about a second.
The proof log [2] is amusing. It's building up number theory from a very low level, starting by proving that X + 0 = X. Each theorem proved can be used as a lemma by later theorems, so you guide the process by giving it problems to solve in the right order. By line 1900, it's proving that multiplication distributes over addition. Array theory, the new stuff, starts around line 2994.
The reason this is so complicated and ugly is that there's no use of axiomatic set theory. Arrays are easy if you have sets. But there are no sets here. Sets don't fit well into this strict constructive theory, because EQUAL means identical. You can't create weaker definitions of equality which say that two sets are equal if they contain the same elements regardless of order, because that introduces a risk of unsoundness. Effort must be put into keeping the tuples of the array representation in ascending order by subscript, which implies much case analysis. Mathematicians hate case analysis. Computers are good at it.
[1] https://github.com/John-Nagle/nqthm
[2] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
This is true, but a similar problem plagues typical proofs.
> Proofs need to be dense enough that we can discover them in a long lost tomb and eventually figure out what that collapsed civilization had learned.
This is almost never the case for modern mathematical research. Case in point, some of my current work relies on the classification of finite simple groups. Therefore, in practice, it is impossible to validate my results from first principles.
https://retractionwatch.com/2022/11/18/mathematician-request...
https://retractionwatch.com/2017/07/12/author-shocked-top-ma...
Prof. Byron Cook (pure math at UCL) is arguably a driving force behind a lot of the recent adoption of theorem provers. He's talked a lot about those problems (in fact, I was partially paraphrasing him from memory above). You can read up on what he said directly, I found it pretty convincing that proof verification is where modern mathematics should be moving towards (and probably will, there are collaborative efforts to re-prove substantial parts of modern mathematics using automated provers).
Btw, do you have any support for your claim that proofs must be dense enough to fit onto a tombstone? I've literally never heard that before, and by your definition, pretty much no recent mathematical research would qualify. We've come a long way since Euclid.
I'm not a mathematician, but I have at times been able to consider myself a computer scientist. To me, the goal of "mechanizing" and formalizing mathematics seems instinctively recognizable as a worthwhile pursuit, for the same reason it's worth adding tests to an unwieldy legacy codebase: it makes it possible to refactor, to experiment and break things and see what happens.
The more we formalize the most fundamental axioms and theorems of mathematics, the more confidently we can alter or remove them and see what happens to the rest of the system. Achieving "100% test coverage" and "instrumentation" of mathematics would allow us to analyze the system under stress. We could fuzz it. We could refactor it. We could even ask an AI to do that for us.
As a relative layman, I'm often struck by how many mathematical theorems are dependent on the arbitrary paths we took to develop them. For the same reason, it's a common occurrence that one mathematician discovers an innovation in one branch of mathematics by simply borrowing a common technique from a distantly related branch. Those sorts of analogies and connections between ideas are difficult for humans to spot, and their discovery scales linearly with the number of mathematicians, who might prefer to spend their time discovering truly new ideas rather than repurposing those already existing ideas.
But computers, on the other hand, are excellent at spotting these relationships, if given sufficiently formalized definitions of them. So that's why I'd be most excited about formalizing mathematics: how much low-hanging fruit is waiting to be discovered by computers that are just missing the right prompt?
Concerning analogies and borrowing techniques between fields, this is absolutely something humans are good at and which it is very hard for computers to do. Why do you think otherwise? To take a very simple example, most mathematical objects can be represented in different ways. A mathematician can fluently move between these representations, whereas computers cannot. This is a largely the obstacle for the adoption of proof assistants among mathematicians.
I agree that humans are better at borrowing techniques between fields, but we can't do it quickly, and we can't systematically mine the entire "codebase" for these relationships (hence why "discoveries" in 2020 can combine ideas from 1990 and 2000). Besides, I suspect much of that gap between human and computer ability is due to a lack of a properly formalized representation of the ideas within each possibly related field. To use a programming term, it's a "code smell" if we haven't properly encoded the relationships between two fields. Sure, we can manually identify them, and then build on them once we do. But why did we need to bother in the first place? Wouldn't a formal system have made the relationships obvious, or at least more automatically discoverable?
Large language models have also changed my view of what computers are capable of, and in that context I've been most impressed with their ability to analogize and explain relationships between seemingly arbitrary sets of ideas. It makes sense they'd be good at this, since the premise of training them is to construct a web of weights that's indecipherable to humans but fundamentally enabling to the language model. Stephen Wolfram has been writing about how language models seem to encode a certain "truth" which has always existed but which we've never recognized. This idea resonates with me and I expect models have a lot to teach us about our own consciousness and how we model the world.
But on the other hand, if LLMs are so successful, by definition, at identifying relationships without being given formal representations of them, then why bother formalizing mathematics? After all, mathematics only exists because we can communicate its ideas by constructing the language of mathematics as a sort of amalgam of spoken language and abstractions we create within it. And while the exercise of formalizing the relationships between those abstractions might identify some imprecisions or mistaken assumptions in the existing hybrid of spoken language and formalized chunks of math, do we really need to bother? For an advanced LLM, shouldn't our existing definitions become naturally encoded into its weights during training, so that any emergent formalisms can be poked and prodded when we talk to it or ask it to reason about them? Or will it get stuck on the same imprecisions that we might identify when trying to manually formalize our existing systems of mathematics?
Imagine if someone discovered a way to solve real world problems by formulating them as chess positions. Would it be reasonable of us to demand that chess players stop competing and work on these formulations? No, and I don’t think many chess players would jump at the opportunity. They just want to play chess!
Experimenting with axioms is one way you discover more math. For example, set theory: there’s a lot of math assuming ZF(C), but even more if you start looking at alternatives to it (like NBG, NF(U), constructive set theories, non-well-founded set theories, paraconsistent set theories, etc)
What would help dramatically for me and others that work in applied math are proofs that cover the material in something like Principles of Mathematical Analysis by Walter Rudin. These are proofs that cover basic real analysis and topics like continuity, differentiation, and integration. It would also help to see basic linear algebra proofs such as that all real symmetric matrices have a real eigendecomposition. Now, these may exist and it's been a couple of years since I've looked. If anyone has a link to them, I'd be extraordinary grateful.
I'm curious, which field of math do you work in?
Edit: for example, that symmetric matrices have real eigenvalues is shown here in mathlib: https://leanprover-community.github.io/mathlib_docs/analysis...
Generally speaking, I work in the intersection between optimization, differential equations, and control. To that end, there's a variety of foundational results in things like optimization theory that I'd like to see formalized such as optimality conditions, convergence guarantees, and convergence rates.
Two questions if you know. One, which theorem prover would you recommend for working toward these kinds of results? Two, is there appetite or a place to publish older, known theorems that have been reworked and validated? And, to be clear, two is not particularly important for me and my career, but it is for many of my colleagues and I'm not sure what to tell them about it.
I'm afraid I have no knowledge of your field, and no idea whether there are good tools and libraries for formalising the things you want. Maybe ask or have a look around the Proof Assistants StackExchange[1]?
There are many CS conferences through which you can publish formalised mathematics. One that comes to mind is ITP[2], but there are lots which are announced on mailing lists like TYPES-announce, coq-club, agda... You could look through previous versions of ITP and check out a few of the papers on formalising mathematics to get a feel for what these publications look like.
[1] https://proofassistants.stackexchange.com/
[2] https://mizar.uwb.edu.pl/ITP2023/
There are two very different directions 1. the sort of full on proof automation with tactics https://direct.mit.edu/books/oa-monograph/4021/Certified-Pro... Dr. Chlipala builds up understanding of the "crush" tactic, which more or less lets you specify an inductive hypothesis, and that tactic fiddles around with identifying the base case, and expanding enough to generate the n+1 step. Along the way, you get exposure to using Gallina to write your own tactics.
it's neat, from a programmer point of view, because you can automate away the boring parts. There is pretty good discussion of debugging tactics, which might provide a path to transforming machine proofs into something a bit more comprehensible. at the very least, you can recover the application of axioms and such that did the transformation.
The other direction, that has been much more enlightening for me (the amateur hobbyist) was agda and Jesper Cockx's tutorial- https://github.com/jespercockx/agda-lecture-notes/blob/maste... he builds up all of the notation from, well, nothing. for example, you get refl, and then build up
along with the syntax that comes with the agda std lib. agda is different, but you can still extract to Haskell (and allegedly javascript for node, but that was a little flakey for me and might go away in a future release). less useful for your goals, much more programming oriented - https://plfa.github.io is pretty good, and worth mentioning as a reference.Which raises an interesting philosophical question - do contemporary mathematicians mostly do things one way rather than another (i.e. classical logic instead of intuitionistic/paraconsistent/etc logic, ZF(C) set theory instead of alternative set theories or type theory or whatever, classical analysis instead of non-standard analysis, and so on) - because they’ve settled upon the inherently superior (easier, more productive) way of doing things - or is that just an accident of history? Could it be that in some alternative timeline or parallel universe out there, mathematics took some different forks in the road, and the mathematical mainstream ended up looking very different from how it does here?
Last time I commented about this [0], I made some guy irrationally angry as he told me I sounded like I was 19 years old. And in an earlier comment [1], another guy took extreme offense to my questioning of the statement "with enough marbles, the discrete distribution behaves like a continuous distribution."
It seems there is some high priesthood of mathematics and physics that doesn't like when you ask these sorts of questions.
[0] https://news.ycombinator.com/item?id=35018407
[1] https://news.ycombinator.com/item?id=35201603
If people make comments like that, flag them and email dang (hn@ycombinator.com) and he’ll do something about them
> It seems there is some high priesthood of mathematics and physics that doesn't like when you ask these sorts of questions
In my personal experience, most professional mathematicians and physicists are open to questioning the foundations of their discipline, and deal charitably with doubters (even those who are coming from a place of misunderstanding).
I suspect most of the “high priests” you speak of aren’t actually professionals at all, just Internet randoms who (at best) know only slightly more than you do, and who know very little about the norms of civil dialogue
In other foundations, such as homotopy type theory (which is what the article is about), the distance between "informal" mathematical arguments and their formal counterparts is much shorter. This is why formalisation is widespread in the HoTT-community. Indeed, I believe Voevodsky worked on HoTT in order to have a foundation which was much closer to the mathematical practice in homotopy theory.
Computer programs are useful. Bigly. So we develop infrastructure around them.
Are mechanized proofs useful? Are they intelligible? Do they grant insight? Do they work better?
As for your other questions: No, formal proofs are not intelligible to the average mathematician. They do not on their own grant insights, but the process of formalising a proof does often yield insights. (I speak from experience.) Not sure what you mean by "better"; they certainly don't replace ("informal") mathematical proofs.
So where does this lead? As you build a large database of formalized mathematics you get some snowball effects. We can train language models just like on code to assist us. Formalizing natural language mathematics should merely be a process of translation, if set up correctly, not somwthing computationally advanced. Copilot for formal maths will being the constant lower. As correctness of formal proofs can be automatically checked, at some point you can let the system attempt formalizing Pdf documents by itself. This yields you a larger database, more traininf data etc. In 20 years I hope that we have a database of most.mathematics formalized in Lean, and language models that can translate between natural language math and Lean quite fluently. As any formal language of mathematics is also a programming language, we van start doing some very serious program correctness validation. You will not just run your Euler iteration until it has sufficiently small error, but you will instead run it up to your PROVEN desired error. Because we did all the work of formalizing mathematics, this will not be much harder than just writing the program normally. Mathematicians can also now work with these systems and thereby work quicker, saving time on reviews. Computer verified proofs will.not be unreadable, the database will be open source and constantly refactored and kept clean. Etc. Etc.
Are computer programs written this way?
No. (Or not yet.)
UniMath (https://github.com/UniMath/UniMath, mentioned in the article)
Coq-HoTT (https://github.com/HoTT/Coq-HoTT)
agda-unimath (https://unimath.github.io/agda-unimath/)
cubical agda (https://github.com/agda/cubical)
All of these are open to contributions, and there are lots of useful basic things that haven't been done and which I think would make excellent semester projects for a cs/math undergrad (for example).
Unfortunately, Voevodsky, the "hero" of this piece, died in 2017.