Presumably people who get into math going forward will feel differently.
For myself, chasing lemmas was always boring — and there’s little interest in doing the busywork of fleshing out a theory. For me, LLMs are a great way to do the fun parts (conceptual architecture) without the boring parts.
And I expect we’ll such much the same change as with physics: computers increase the complexity of the objects we study, which tend to be rather simple when done by hand — eg, people don’t investigate patterns in the diagrams of group(oids) because drawing million element diagrams isn’t tractable by hand. And you only notice the patterns in them when you see examples of the diagrams at scale.
Just a counterpoint, but I wonder how much you'll really understand if you can't even prove the whole thing yourself. Personally, I learn by proving but I guess everyone is different.
My hunch is it won't be much different, even when we can simply ask a machine that doesn't have a cached proof, "prove riemann hypothesis" and it thinks for ten seconds and spits out a fully correct proof.
As Erdos(I think?) said, great math is not about the answers, it's about the questions. Or maybe it was someone else, and maybe "great mathematicians" rather than "great math". But, gist is the same.
"What happens when you invent a thing that makes a function continuous (aka limit point)"? "What happens when you split the area under a curve into infinitesimal pieces and sum them up"? "What happens when you take the middle third out of an interval recursively"? "Can we define a set of axioms that underlie all mathematics"? "Is the graph of how many repetitions it takes for a complex number to diverge interesting"? I have a hard time imagining computers would ever have a strong enough understanding of the human experience with mathematics to even begin pondering such questions unprompted, let alone answer them and grok the implications.
Ultimately the truths of mathematics, the answers, soon to be proved primarily by computers, already exist. Proving a truth does not create the truth; the truth exists independent of whether it has been proved or not. So fundamentally math is closer to archeology than it may appear. As such, AI is just a tool to help us dig with greater efficiency. But it should not be considered or feared as a replacement for mathematicians. AI can never take away the enlightenment of discovering something new, even if it does all the hard work itself.
> I have a hard time imagining computers would ever have a strong enough understanding of the human experience with mathematics to even begin pondering such questions unprompted, let alone answer them and grok the implications.
The key is that the good questions however come from hard-won experience, not lazily questioning an AI.
Even current people will feel differently. I don't bemoan the fact that Lean/Mathlib has `simp` and `linarith` to automate trivial computations. A "copilot for Lean" that can turn "by induction, X" or "evidently Y" into a formal proof sounds great.
The the trick is teaching the thing how high powered of theorems to use or how to factor out details or not depending on the user's level of understanding. We'll have to find a pedagogical balance (e.g. you don't give `linarith` to someone practicing basic proofs), but I'm sure it will be a great tool to aid human understanding.
A tool to help translate natural language to formal propositions/types also sounds great, and could help more people to use more formal methods, which could make for more robust software.
For myself, chasing lemmas was always boring — and there’s little interest in doing the busywork of fleshing out a theory. For me, LLMs are a great way to do the fun parts (conceptual architecture) without the boring parts.
And I expect we’ll such much the same change as with physics: computers increase the complexity of the objects we study, which tend to be rather simple when done by hand — eg, people don’t investigate patterns in the diagrams of group(oids) because drawing million element diagrams isn’t tractable by hand. And you only notice the patterns in them when you see examples of the diagrams at scale.