Accelerationists may argue that the eroding of proper attribution and proof verification by humans is a meaningless short term struggle of a dying field. Mathematics seems to be entering an era where human + machine maximizes performance, much like chess in the 1990s. However, imagine a future where even talented mathematicians are nothing but noise in the machine (as is the case in chess now). A future where AI generates and verifies proofs without humans in the loop. Where the mathematics may be beyond human comprehension. In that future, does it matter that early career mathematicians are inhibited by these developments? Perhaps not. Programming faces the same issue. As AI crawls up the competence ladder, does it matter that fewer people have opportunities to develop the skillset of a senior engineer? Perhaps not.

Neural networks are already systems of linear algebra that are beyond human understanding. Most humans could probably grok a 1 or 2 dimensional slice of a network, but the latent vector space is completely beyond the human brain. We have to use tools to analyze neural networks piecemeal in exactly the same way that we analyze any other higher-dimensional construct. Few humans are truly capable of reasoning in 4+ dimensions, that doesn't make string theory "not math". Nor does a trillion-dimension vector space of an LLM make it "not programming". Humans by themselves invented mathematical concepts beyond human understanding a long time before we invented neural networks.

Is it still chess, if humans cannot understand it? Because that's the point we are at in chess. Engines making moves, that humans cannot understand, but somehow they work out to be best or seemingly best. Look at the Leela Zero games, when it came out. These engines play kind of other-worldly chess.

I think there would still be a place for it if it's beyond human comprehension. For instance, really complex lemmas to solve human-tractable problems. If you can pose a question in a proof assistant language like Lean, have an AI write a Lean program that solves it, you can use that as a Lemma for some other problem. There's quite a bit of math out there that is "correct assuming conjecture X is correct", maybe AI could fill that gap and "still be math".

Perhaps P=NP. The new algorithms are handed down to us. We can apply them without fundamentally understanding why P=NP.

To further this assertion, there is almost no value to deeply esoteric math that is technically correct, but completely inapplicable to any scientific reality, and completely unintelligible to humans. Consider these findings deep, dark corners in the unfathomably large hyperspace of mathematics. My guess is AI will be incredibly adept at identifying these types of findings, and it will be exceedingly difficult for humans to identify what is meaningful and what is not in the slop.

Do AIs produce answers whose work is incomprehensible to humans? It seems like you could just have the AI elaborate multiple times until you were satisfied with the explanation and documentation of what went into figuring out the answer. It’s not like the AI is one shotting the answer in a single opaque query anyways.

Like other commenters, I think you’re also underestimating the complexity of esoteric higher level math. Consider the “Magnus Carlsen” of mathematics, who is more capable of understanding mathematics than any other human. But then also realize that that individual has probably devoted their entire career into a specific subdomain of mathematics. Within other deep recesses of mathematics, this Magnus equivalent will be less capable than their peers without years of rewiring their brain to understand the esoteric concepts and properties within that other subdomain. LLMs will be able to dig deeper and broader than any human mathematician, and find results that are completely useless to humans because it would take more than an entire lifetime to “speak the language” of the concepts the LLMs have produced. The only way those results can become useful to humans is if then the LLM itself finds a way for it to be practical to humans once again. So, no, I don’t think this represents the “democratization” of mathematics where mathematicians are no longer necessary because anyone can just prompt the LLM to explain it. The bar for entry level mathematics is lower, for sure, but research level mathematics will continue to be unapproachable for anyone who hasn’t devoted their career to it.

Micromanagement wasn't the message I took from that. Rather the level of human involvement required which (it seems like) the two of you more or less agree on. The meaning I took was how far it's possible to travel from the shore - ie the scope of the state space. The mathematics we're exposed to is all quite shallow compared to what will (presumably) be possible between digital formalization and massive ML models. But the latter probably can't ever be understood by regular biological humans.

How do you make use of something that you don't understand?

For most engineers a mathemetician is a machine for producing correct algorithms, like a chef is a machine for producing tasty food. In both cases that overlooks the human element, but that's a critical skill for a limited mind with finite resources to grok infinite complexity. You can read that as permission to be an asshole or a neccesary compromise.

Math is one field where you can mechanically prove a paper's findings. The only thing that would need to be judged is the (verified) statement's importance.

>> However, the declaration argues math is more than a machine for producing correct answers. > There might be more to maths than that, but that is definitely the most important part. I love science funding. But not because it's a jobs program for nerds. I can produce an infinite number of verifiably correct papers, if that's all that matters. 1 + 1 = 2 1 + 2 = 3 1 + 3 = 4 1 + 4 = 5 1 + 5 = 6 Shall I continue? Or do you think that choosing which questions to answer might have some level of importance, in addition to getting correct answers?

A statement that some proposition is true or false is usually less useful than a new framework for understanding the class of problem. A machine that takes longer and longer to prove propositions in ever more inscrutable ways is hardly useful at all. The machine too needs to produce more generalizable and comprehensible systems, for it to scale up its own conceptualization. Needing to load all the new mathematics in the context window won't be great either.

Even from the most purely instrumental perspective, what we care about is our ability to make use of correct answers, which is quite distinct from the possession of correct answers. There are many theorems that aren't directly interesting, but whose proof requires techniques that are of substantial further interest, that lead to new domains, and/or new practical applications. Simply being handed a proof for those theorems isn't enough--we require the ability to apply those techniques in the real world, or discover further areas of mathematical research that build on that proof or its techniques. It may be that AI can build on its own work for the long-term, but so far, AI does best at exploration in areas that have precisely specified and measurable goals. Actually creating understanding, and making use of mathemtical results outside of pure mathematics is more challenging than simply creating proofs. I think the field will figure out how to make use of AI, and it will be better off for it. But that is not the same as just saying "answers good, grog want more answers."

Understanding is and always has been the "hard" bottleneck. In programming work, if one drops understanding and eg let's an agent write code with only superficial human review or none at all, I believe that they can easily get 100x fast or more, the main question being whether the process collapses some point due to sloppy code. In research fields like mathematics, skipping understanding is not something that can be done without a radical reconstruction of what mathematics (as a process/activity/field) is. It sounds plausible that LLMs help generate insights that humans have missed. But there are many open questions, eg the rate of generating insightful vs uninsightful but plausible statements, which can affect how useful they will be, and of course "open"ai has no incentive to share how much effort/cost (tokens and/or human-review) had been put into investigating erdos problems before coming up with this solution.

I think the bigger issue is that mathematicians historically invented the abstractions to make maths easier to understand for humans. With LLMs, will we get abstractions that only computers can understand?

Does it matter whether any of this is correct? (Mathematics at least has the potential for automated non-AI proof checking, although I don't think that's as widely used as you'd expect)

Does it matter if the Leiden Declaration is correct? To the humans, maybe but not in the bigger picture. At scale, correctness and reward are becoming increasingly disconnected. Example: capital continues to compound regardless of whether it reflects underlying human welfare, just as information can spread regardless of whether it is true. Reality still matters, of course. If you want airplanes to stay in the air, somebody eventually has to be correct. The problem is that our economic and social systems are becoming less effective at distinguishing between what is true and what is merely rewarded.

It's more nuanced than this. Peter Scholze said in response to this declaration: > The goal of mathematical research is human understanding of mathematics, and so mathematics can only thrive in a community of human mathematicians. It is crucial to preserve this communal spirit. [0] Terence Tao has also talked about the requirement for a mathematical proof: along with generation and formal verification, there is an important step of "proof digestion" > understanding the essence of a solution, placing it in context with previous literature, summarizing and explaining it effectively, and gaining insights on other related problems and topics [1] [0]: https://siliconreckoner.substack.com/p/the-leiden-declaratio... [1]: https://mathstodon.xyz/@tao/116450581967483825

Solve it and understand it; seems intuitive to me. I don't understand how that contradicts my question.