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