Will Computers Redefine the Roots of Math?

> 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.

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:

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 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.

> 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)

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?

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.

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.

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

> 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.