What does it mean to be a mathematician when AI does the math?
15 points by veqq
15 points by veqq
Frankly, as a mathematican, I'd probably rather quit than play the verifier for some AI. The cool thing about being an academic and not an engineer is that not everything has (had?) to be faster, faster, FASTER (though this also heavily depends on you area/research group). You actually have time to think sometimes. The joy is the dead ends, the struggle, the talking and thinking with other people... THAT's maths. Not reading some random proof produced by a machine.
Sure, sometimes it's faster to ask the clanker an easy question and verify that the proof is correct than to sit down for 30 minutes and just think (not to mention it feels so much easier). But why? Where's the joy there? If I was interested in outcomes I wouldn't be doing pure maths in the first place. (Not to mention you don't nearly learn as much, but that's a whole different story)
Though frankly I'm also not in the business of caring about (much less being competent enough to contribute to) these hard and famous problems and their solutions all that much; perhaps it's more interesting for people who do. A classic Grothendieck vs. Erdős division, I guess.
What does it mean to be a computer scientist when the compiler writes the code? In some ways these discussions are just so stupid. Nothing has changed! Abstraction did exist, and it does exist. Intelligence did exist, and it does exist. Heuristic output of text did exist, and it does exist.
Just remember this: if AI ever seems intelligent, it's only because people were first. People had to put their reputation at stake for society to make progress. Even if those people have had their voices stolen by a robot, it was only ever the people who really created the value
What does it mean to be a computer scientist when the compiler writes the code?
The compiler doesn't write the code, it applies advanced macro expansions to the code. The explicit goal of AI, regardless of whether you believe AI is currently able to meet its goals, is to short-circuit the need to understand the problem.
Even if those people have had their voices stolen by a robot, it was only ever the people who really created the value
I'm not sure that endorsement of theft is matches the attempt here at a comforting tone. But also I'm not sure if this entire post is meant to be subtle sarcasm. The account name may point towards it.
Optimising compilers do «advanced macroexpansion» using things that counted as AI before the latest (hopefully not the last) AI Winter.
And some of the previous-definition-of-AI tools invented novel mathematical constructions to resolve Robbins conjecture.
(Understanding an alien construction is sometimes easier than inventing; I also have a pre-LLM experience of writing a follow-up to a paper with a bruteforce construction authors didn't claim to understand except formally, but analysis of generalisability called for understanding this thing — which was doable)
I'm not sure that endorsement of theft is matches the attempt here at a comforting tone.
I agree that LLMs being bad at keeping track of sources is in fact bad in terms of their output. If the were better, it would be a useful tool for literature search (still with a problem of, let's say, «not consistently candid» operators, although plain search engines also have that problem nowadays). And resolving combinatorial geometry problems with literature search — followed by hammering of technicalities that everyone calls boring — has some precedents.
For smaller things, however, computer algebra systems don't seem to credit the authors of each integration method, so I think there are limits for what kinds of rewording-without-source-reference you can maintain a noticeable level of criticism.
fwiw I don't read that as endorsement so much as indictment, but tone in text is mostly hard
Good article. Programmers could certainly take a page from mathematicians and reflect on where their craft is going, with an open mind.
You don’t have to be the first one to do a proof to enjoy it. You don’t even have to do it de novo. Every few years I revisit cantor’s diagonal argument or the infinity of primes, pythagoras’ theorem.
It’s like reading a loved book.
Now imagine all the wonderful new proofs that we will have the joys of looking at.
Personally I find those proofs elegant and beautiful because I know their discovery is the product of the human mind, like a form of art. AI-produced proofs won’t have the same appeal.
I don't feel that myself, and I wonder why this is.
Your use of the word 'discovery' for mathematics is my preferred bias for the classic question as to whether math is discovered vs invented. And, at least for me, discovery is an accretive benefit, no matter the source.
I think the journey towards the discovery is important as well. That’s why popular science books are full of the life story of scientists as well as their discoveries. Of course a proven theorem is more useful than an unproven one. But will not be beautiful or elegant in my eyes. Or maybe I just have to get used to the phenomenon.
I enjoyed this because it was nuanced and had good detail, yet didn't attempt to arrive at a definitive answer. No one actually knows where we'll end up with AI, but wrestling with questions about it is still worthwhile.
Some worry about the accessibility of AI tools. [...] mathematics could become an elitist activity, only practiced by select organizations that can afford to work with proprietary AI models.
(I liked how this brought in accessibility. I've seen some discussions of AI and accessibility, and how some people feel that e.g. banning AI in projects hurts accessibility, but I've not seen this framing of accessibility as the literal ability to access these large cloud-based models. For me, that's probably the most salient practical concern).
Another concern is motivation. As AI systems take on more of the work, the incentive to engage deeply with difficult problems may weaken. [...] “If your computer can do large chunks of that for you, will you have the motivation to spend that time?”
That concern extends to the next generation. If students can use AI to jump straight to answers, they most likely will. [...] Over time, some worry, the next generation of mathematicians may suffer from a form of intellectual atrophy [...]
I worry about all these too, though in my case for programming, and beyond. This could really wreak havoc on many fields in the long term, and pretty much everything else as a knock-on effect (or maybe we'll be fine).
And yet we now have this technology that can automate mathematical proofs, reason through complex ideas, write non-trivial code, and do other things that are honestly deeply cool (and jarring at the same time).
I've flagged this as off-topic because of this guideline:
Topicality: Lobsters is focused pretty narrowly on computing; tags like art don't imply every piece of art is on-topic. Some rules of thumb for great stories to submit: Will this improve the reader's next program? Will it deepen their understanding of their last program? Will it be more interesting in five or ten years?
I've been writing term writing systems/compilers for lamba calculus, SMT solvers and such lately. There's quite a difference between calculating values and converting equations to normal form (lambda calculus e.g. can't rewrite (= (+ a b) (+ a c)) to (= b c) because of orientation. Calculating doesn't have so much direct use in mathematics as such, but a lot of cool computer science lets you do deductive/algebraic reasoning via computation. These "reasoning agents" are similar, generating massive baroque proofs... For a long time, mathematicians ignored (proof) solvers etc. for not actual increasing understanding... We have long faced the same issues with cognitive debt, turning implicit knowledge to more tacit forms, so... I found this extremely topical. What are we even doing?
… and the best-case SMT-solver-found invariants are even more understandable than constructions in the worst human-written-and-published proofs of upper/lower bounds!
I find it very strange that someone could consider this article unrelated to computing. I can't imagine it's because it's about the role of AI in the practice of mathematics, because I can't imagine you'd disagree that math is unrelated to computing, given your username. I'm asking in good faith and with genuine curiosity