Mathematics Without Mathematicians

We will become students of AI mathematics.”

This works until the AIs have blasted so deep into the deductive closure of mathlib that the distance from elementary mathematics to the frontier exceeds what any human can hope to learn in their lifetime, no matter how narrow their focus.

It is already the case that mathematicians don't learn all the math there is to know -- there's far too much of it. In fact, workers in one area of math often won't be able to follow talks given by workers in an other area. Some broad strokes might be understood but even outside the basic theory of a field there are all the colloquialisms and bits of tribal knowledge that nobody has ever bothered to write down.

And the map is not the territory, as they say -- the author is getting lost in the "frontier" analogy. The frontier doesn't work like a geographical frontier and I doubt there's any heuristic metric for the distance between what is elementary and research level problems that would match your intuition for how the frontier moves as new problems are solved. Rather sophisticated advances lead to problems that don't necessarily require much machinery to understand or even solve. Sometimes the frontier means building bridges or alternate mappings between different fields so that new tricks and tools are available

Some of the author's counterpoints are well made but I don't get the impression that this person knows very much about mathematicians or what they do. I also find that pushers of maximalist takes like this often from like they would benefit a bit from a few careful close readings some good critiques of modernity.

We won’t! This misunderstands who the audience will be. AIs will do frontier math, downstream, AIs will use the new math to do frontier science, finally, AIs will use the new science to do frontier engineering. No human needs to understand any of it, firms that put humans in the loop to understand the results will be outcompeted by those which don’t.

I think this misunderstands math as a field. While some mathematical research is aimed at doing science and engineering, a ton of it is pure research without immediate application. Most mathematicians have understanding as the goal, not an eventual gadget. So I think it’s unlikely we’ll bypass this step all that quickly.

As an aside:

AIs will use the new math to do frontier science, finally, AIs will use the new science to do frontier engineering

I am once again begging software engineers to learn more about physical-world science and engineering. As much as theory and simulation help with science, actual measurement and experimental data is slow and tedious and necessary.

Yes, yes, robots — given the level of human support existing robots need, I’m very skeptical we will see fully-independent AI engineering being done outside pure computation. Humans are going to be in the loop for a long time.

One thing I'd say about AI developed math is that we still don't know what it looks like in a few years.

All the results that we've seen so far involve combining existing concepts and techniques. There is a level of creativity to it, and the contributions are real. You can have a full career as a mathematician doing nothing that's more difficult than what the AIs can do.

However, that's not all that there is to math. Developing new unifying abstractions, concepts and proof strategies is a major way that the field progresses. I'm not saying that AI necessarily can't do that, but it hasn't done it yet, and it's at least plausible that it isn't yet able to do so (it requires a different kind of thinking, one that also requires very long term investigation that AI is not necessarily great at).

Basically, I'm not betting against AI, but just as the huge changes in software haven't yet yielded systems that can replace software engineers, I'm don't think we have systems yet that can replace mathematicians. Maybe next year. Maybe not for a while.

I'll be watching...anxiously.

The arguments here are somewhat portable: replace "mathematics" with "botany" or whatever as needed.

Okay. The biggest unsolved problem in botany is Darwin's abominable mystery: How did flowers evolve so quickly? This immediately suggests a reason why the article's arguments aren't portable, namely that results in mathematics and botany have differing standards of evidence and proof. No answer to Darwin's mystery can be more than a narrative story which we tell each other in order to understand the historical and archeological records; by starkest contrast, a mathematical proof is a sequence of rule applications which can be mechanically verified in polynomial time.

At some point, the human pointing the way will get worse results than the human saying “here’s a proof checker, have fun” and paying for the tokens.

Proof search is NP-hard. Chatbots do not magically change how complexity theory works. If you want to hook an RNG up to Lean then there are more direct and satisfying ways to do it. (Also, looking at this from another direction, Idris has had type-driven completions for like half a decade; chatbots can't even use tab-completion!)

The AIs are explorers out in the frontiers, the humans gratefully receive their Lean proofs, and then discourse over them, choose which results are relevant, shape those results into a little brick for the great cathedral of algebra.

Lean isn't even the biggest such cathedral; from Formalizing 100 Theorems, Isabelle and HOL Light have been in the lead the entire time. The author does a lot of dependent-type-theory work but I suppose that they aren't really paying attention to how mathematics is formalized; I would love to read their cope over the presence of Metamath on that page. Even better, I dare them to ask a chatbot to generate Metamath proof statements; I already learned a few years ago that this is an NP system which doesn't yield valid useful proofs quickly.

will live in a demon-haunted world, full of marvelous devices whose operation we will not understand

This has been the perpetual state of humanity since Mogg grabbed that flaming branch.

but the result, in the long run, is that humans become, at best, like pets under the care of vastly more powerful entities.

I don't find it difficult to accept. Should humanity finds itself incapable to sort things out together, amicably, into a stable enough socio-political equilibrium, to be put into zoos or getting domesticated is a great mercy indeed, than getting turned into lab test subjects (or cattle, livestock or worse, for that matter), or outright "optimized away" (annihilated).

On the other hand, in case our consciousness be capable enough to evolve to be able to accomodate AGI in it, to form such hybrid entities, I wonder what would that look like. From "pure" AGI independent of human intellectual inheritance, to a human consciousness with a subordinate AGI, or vice versa, and everything in between, taking various elements of AI and human consciousness and mixing them in different quantities and arrangements, in some kind of consciousness chemistry (ugh) and so on. Sigh, whatever I'm blabbering about here.. what manner of ethical and moral troubles would such stuff invite..

Let's see how it goes.