Like I said, I don't have any idea what's going to happen. The thing that makes me sad about these conversations is that the people I talk to sometimes don't seem to have any appreciation for the thing they say they want to dismantle. It might even be better for humanity on the whole to arrive in this future; I'm not arguing that one way or the other! Just that I think there's a chance it would involve losing something I really love, and that makes me sad.
Oh… I didnt anticipate this would bother you. Would it be fair to say that its not that you like understanding why its true, because you have that here, but that you like process of discovering why?
Perhaps thats what you meant originally. But my understanding was that you were primarily just concerned with understanding why, not being the one to discover why.
I can only speak for myself, but it's not that I care a lot about me personally being the first one to discover some new piece of mathematics. (If I did, I'd probably still be doing research, which I'm not.) There is something very satisfying about solving a problem for yourself rather than being handed the answer, though, even if it's not an original problem. It's the same reason some people like doing sudokus, and why those people wouldn't respond well to being told that they could save a lot of time if they just used a sudoku solver or looked up the answer in the back of the book.
But that's not really what I'm getting at in the sentence you're quoting --- people are still free to solve sudokus even though sudoku solvers exist, and the same would presumably be true of proving theorems in the world we're considering. The thing I'd be most worried about is the destruction of the community of mathematicians. If math were just a fun but useless hobby, like, I don't know, whittling or something, I think there would be way fewer people doing it. And there would be even fewer people doing it as deeply and intensely as they are now when it's their full-time job. And as someone who likes math a lot, I don't love the idea of that happening.
Why would mathematics be different than woodworking?
Do you believe there’s a limited demand for mathematics? — my experience is quite the opposite, that we’re limited by the production capacity.
> You’re comparing something many people do as a hobby to the life’s work and f others.
You’re denigrating the talents and educational efforts of artisanal woodworkers to make a shallow dismissal of my point.
One place I think the analogy breaks down, though, is that I think you're pretty severely underestimating the time and effort it takes to be productive at math research. I think my path is pretty typical, so I'll describe it. I went to college for four years and took math classes the whole time, after which I was nowhere near prepared to do independent research. Then I went to graduate school, where I received a small stipend to teach calculus to undergrads while I learned even more math, and at the end of four and a half years of that --- including lots of one-on-one mentorship from my advisor --- I just barely able to kinda sorta produce some publishable-but-not-earthshattering research. If I wanted to produce research I was actually proud of, it probably would have taken several more years of putting in reps on less impressive stuff, but I left the field before reaching that point.
Imagine a world where any research I could have produced at the end of those eight and a half years would be inferior to something an LLM could spit out in an afternoon, and where a different LLM is a better calculus instructor than a 22-year-old nicf. (Not a high bar!) How many people are going to spend all those years learning all those skills? More importantly, why would they expect to be paid to do that while producing nothing the whole time?
- apprenticing
- journeyman phase
- only finally achieving mastery
CNC never replaced those people, rather, it scaled the whole field — by creating much higher demand for furniture. People who never made that full journey instead work at factories where their output is scaled. What was displaced was mediocre talent in average homes, eg, building your own table from a magazine design.
You still haven’t answered why you think mathematics will follow a different trajectory — and the only substantial displacement will, eg, be business analysts no longer checking convexity of models and outsourcing that to AI-scaled math experts at the company.
First, right now presumably the reason a few people still become master woodworkers is that their work is actually better than the mass-produced furniture that you can get for much less money. Imagine a world where instead it was possible to cheaply and automatically produce furniture that is literally indistinguishable from, or maybe even noticeably superior to, anything a human woodworker could ever make. Do you really think the same number of people would still spend years and years developing those skills?
Second, you've talked about business logic and "math experts at the company" a few times now, which makes me wonder if we're just referring to different things with the word "mathematics". I'm talking about a specific subset, what's sometimes called "pure math," the kind of research that mostly only exists within academia and is focused on proving theorems with the goal of improving human understanding of mathematical patterns with no particular eye on solving any practical problems. It sounds like you're focused on the sort of mathematical work that gets done in industry, where you're using mathematical tools, but the goal is to solve a practical problem for a business.
These are actually quite different activities --- the same individuals who are good at one stand a decent chance of being good at the other, but that's most of what they have in common, and even there I know many people who are much more skilled at one than the other. I'm not really asking anyone who doesn't care about pure math to start caring about it, but when I'm talking about the effect of AI on the future of the field, I'm referring specifically to pure math research.
Yes! This is what frustrates my about the pursuit of AI for the arts too.
I see both cases as people who aren’t well served by the artisanal version attempting to acquire a better-than-commoditized version because they want more of that thing to exist. We regularly have both things in furniture and don’t have any great moral crisis that chairs are produced mechanistically by machines. To me, both things sound like “how dare you buy IKEA furniture — you have no appreciation of woodwork!”
Maybe artisanal math proofs are more beautiful or some other aesthetic concern — but what I’d like is proofs that business models are stable and not full of holes constructed each time a new ML pipeline deploys; which is the sort of boring, rote work that most mathematicians are “too good” to work on. But they’re what’s needed to prevent, eg, the Amazon 2018 hiring freeze.
That’s the need that, eg, automated theorem proving truly solves — and mathematicians are being ignored (much like artist) by people they turn up their noses at.
Who is "they"?
Most AI for math work is being done by AI researchers that are not themselves academic mathematicians (obviously there exceptions). Similarly, most AI for music and AI for visual art is being done by AI researchers that themselves are not professional musicians or artists (again, there are exceptions). This model can work fine if the AI researchers collaborate with mathematicians or artists to understand that the use of AI is actually useful in the workflow of those fields, but often that doesn't happen and there is a savior-like arrogance where AI researchers think they'll just automate those fields. Same thing happens in AI for medicine. So the reason many of those AI researchers want to do this is for the usual incentives - money and publications.
Clearly, there are commercial use cases for AI in all these fields and those may involve removing humans entirely. But in the case of art, and I (and Hardy) would argue academic math, there's a human aspect that can't be removed. Both of those approaches can exist in the world and have value but AI can't replace Van Gogh entirely. It'll automate the process of creating mass produced artwork or become a tool that human artists can use. Both of those require understanding the application domain intimately, so my point stands I think.
In my experience, the vast majority is people who are hobbyists or amateurs in those fields, who are looking to innovate in approaches — eg, the overwhelming majority of AI music is hobbyists using models to experiment. Similarly, the overwhelming majority of people using AI graphics tools are making memes or pictures to share with friends.
Those people are poorly served by the artisanal approach and are looking to create more art — they’re not engaging in “savior-like arrogance” but trying to satisfy unmet desire for new music and art. You’re merely being snooty.
> But in the case of art, and I (and Hardy) would argue academic math, there's a human aspect that can't be removed.
This is the pretentiousness I called out (and you completely failed to address):
> That’s the need that, eg, automated theorem proving truly solves — and mathematicians are being ignored (much like artist) by people they turn up their noses at.
Nobody is stopping you from your artisanal proofs — have at it. You’re refusing to do the ugly work people actually want, so they’re solving their problems with a tool that doesn’t involve you.
I actually don't understand your position here or what you think I'm arguing for. My point is that the real musicians, artists and mathematicians (whether they're hobbyists, academics or professionals in industry) are not well served by detached AI researchers just trying to automate their work for them. They need AI researchers to understand their workflows and build tools that elevate them, i.e. bicycles for the mind (or hands?).
Again, I do recognize there may be new fully automated workflows that can come out of AI research too but I maintain that the actual artists, musicians and mathematicians today have a valuable role in guiding that development too.
In mathematics it is just as (if not moreso) important to be able to apply techniques used to solve novel proofs as it is to have the knowledge that the theorem itself is true. Not only might those techniques be used to solve similar problems that the theorem alone cannot, but it might even uncover wholly new mathematical concepts that lead you to mathematics that you previously could not even conceive of.
Machine proofs in their current form are basically huge searches/brute forces from some initial statements to the theorem being proved, by way of logical inference. Mathematics is in some ways the opposite of this: it's about understanding why something is true, not solely whether it is true. Machine proofs give you a path from A to B but that path could be understandable-but-not-generalizable (a brute force), not-generalizable-but-understandable (finding some simple application of existing theorems to get the result that mathematicians simply missed), or neither understandable-nor-generalizable (imagine gigabytes of pure propositional logic on variables with names like n098fne09 and awbnkdujai).
Interestingly, some mathematicians like Terry Tao are starting to experiment with combining LLMs with automated theorem proving, because it might help in both guiding the theorem-prover and explaining its results. I find that philosophically fascinating because LLMs rely on some practices which are not fully understood, hence the article, and may validate combining formal logic with informal intuition as a way of understanding the world (both in mathematics, and generally the way our own minds combine logical reasoning with imprecise language and feelings).
I think they also adjust their heuristics, based on looking at thousands of computer moves.