I'm not a mathematician so please feel free to correct me...but wouldn't there still be an opportunity for humans to try to understand why a proof solved by a machine is true? Or are you afraid that the culture of mathematics will shift towards being impatient about this sorts of questions?
Well, it depends on exactly what future you were imagining. In a world where the model just spits out a totally impenetrable but formally verifiable Lean proof, then yes, absolutely, there's a lot for human mathematicians to do. But I don't see any particular reason things would have to stop there: why couldn't some model also spit out nice, beautiful explanations of why the result is true? We're certainly not there yet, but if we do get there, human mathematicians might not really be producing much of anything. What reason would there be to keep employing them all?
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.
> 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
Yes! This is what frustrates my about the pursuit of AI for the arts too.
This seems obviously untrue: why would they be replicating it if they didn’t want it?
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.
> why would they be replicating it if they didn’t want it?
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.
> 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.
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 think we're actually in agreement with respect to the needs of AI in music and graphics. When I say "AI researchers" I'm talking about people in industrial and academic labs. I consider the hobbyists you describe to be the users (who obviously can also be researchers). It's the desires/needs of the latter that should drive the research agenda of the former.
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.
I don’t think the advent of superintelligence will lead to increased leisure time and increased well-being / easier lives. However, if it did I wouldn’t mind redundantly learning the mathematics with the help of the AI. It’s intrinsically interesting and ultimately I don’t care to impress anybody, except to the extent it’s necessary to be employable.
I would love that too. In fact, I already spend a good amount of my free time redundantly learning the mathematics that was produced by humans, and I have fun doing it. The thing that makes me sad to imagine --- and again, this is not a prediction --- is the loss of the community of human mathematicians that we have right now.
>But I don't see any particular reason things would have to stop there: why couldn't some model also spit out nice, beautiful explanations of why the result is true?
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.
This is an interesting question! You're giving me a chance to reflect a little more than I did when I wrote that last comment.
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.
CNCs and other technology haven’t destroyed woodworking. There’s whole communities on YouTube — with a spectrum from casual to hobbyist to artisanal to industrial.
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.
HN has this very unique and strange type of reasoning. You’re actually asking why would mathematics be any different than woodworking because CNC machines? It’s like aby issue can be reduced to the most mundane observations and simplicity because we have to justify all technology. Professional mathematics requires years of intense and usually, i.e. almost always, in graduate schools and the entire machinery of that. You’re comparing something many people do as a hobby to the life’s work and f others. of course you can have wave all this away with some argument but I’m not sure this type of reasoning is going to save the technocrats when it he majority of people realize what this app portends for society.
No Im not — I’m comparing two fields that range from hobby to professional, both of which I’ve worked in professionally. But for which automation occurred at different times.
> 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.
This is actually a metaphor I've used myself. I do think the woodworking community is both smaller and less professionalized than it would be in a world where industrial furniture production didn't exist. (This is a bizarre counterfactual, because it's basically impossible for me to imagine a world where industrial furniture production doesn't exist but YouTube does, but like pretend with me here for a moment.) I don't know that this is necessarily a bad thing, but it's definitely different, and I can imagine that if I were a woodworker who lived through the transition from one world to the other I would find it pretty upsetting! As I said above, I'm not claiming it's not worth making the transition anyway, but it does come with a cost.
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?
That’s no different than high-end artisanal woodworking, which I would argue is comparable to self-directed, cutting-edge research:
- 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.
Woodworking is very far from my world, so I don't really have any grounds to judge how comparable the two things actually are. I'll say two things instead.
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.
It would be like having the machine code to something amazing but lacking the ability to adequately explain it or modify it - the machine code is too big and complicated to follow, so unless you can express it or understand it in a better way, it can only be used exactly how it is already.
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).
That is kind of hard to do. Human reasoning and computer reasoning is very different, enough so that we can't really grasp it. Take chess, for example. Humans tend to reason in terms of positions and tactics, but computers just brute force it (I'm ignoring stuff like Alpha Zero because computers were way better than us even before that). There isn't much to learn there, so GMs just memorize the computer moves for so and so situation and then go back to their past heuristics after n moves
