All things AI seems to assume that more and faster is better, but there is no justification of that assumption. As a biological counterexample, a tree grown quickly will likely not be as healthy or strong as one grown slowly.
All things AI seems to assume that more and faster is better, but there is no justification of that assumption. As a biological counterexample, a tree grown quickly will likely not be as healthy or strong as one grown slowly.
Now, I think it's the case that professional mathematics spends way too much money on open problems and way less than it should on pedagogy, exposition, mastery, etc. But that has always been a problem, even decades ago (I've been complaining about it my whole life). AI just finally puts pressure on the world to do something about it. I find it relieving, honestly. And I'm an AI skeptic in many other ways; it's not an AI-maximalism thing. I genuinely think the state of the field of mathematics has been something of a disaster for a long time (thanks, largely, due to the academic incentive structure which heavily favors novel results, no matter how esoteric).
I think the value comes from having people who have built very good intuition in a way that allows them to give explanations that make their ideas (new and old) accessible. Of course the most cutting edge math has become completely inaccessible for even many mathematicians, but at the same time, we've made massive progress in this regard. A hundred years ago college students might barely see calculus, and only serious researchers would see something like group theory. Today, many college students that aren't even math majors learn group theory and (we hope that) this gives them cognitive tools that they can apply in other situations (ability to axiomatize a concept, abstract reasoning etc).
The concern with how these tools are being used is that the current push by AI companies to solve math problems by chucking LLMs at them and producing a proof in Lean, and then using that as currency in the media to increase their stock value, undermines this process because it produces "proofs" without producing the understanding that actually allows humans to think better. All of this is then marketed as being the same as doing mathematics which it manifestly is not. If mathematicians lose the media war though, we'll have a generation of people who believe "math has been automated" and are unlikely to put in the effort to learn how to think for themselves.
To the extent that this event is intending to help the mathematical community find ways to use LLMs in pursuit of improving human understanding and intelligence, as the organizers seem to say it is, I think it's a very laudable goal. But I don't really see how this event is supposed to do that. It sounds a lot more like another fundraiser for team "isn't it cool that AI can produce useless chunks of computer code that compile to prove statements that the vast majority of the people commenting on these results don't even understand." For example, if it's really about finding ways to use LLMs to produce mathematics that improves human understanding, why is there even a requirement to solve a new problem? Why not make it explicitly about using LLMs to produce pedagogical content? Or if you really want it to be a new problem, why not add a requirement that the final product has to be accessible to a broad audience (say relying only on material in the undergraduate curriculum)?
P.S. There's another scenario where "not solving the problems" is morally justifiable: the scenario where the "solution" provides very little value (say because of what I said above - the solution just being a Lean artifact that adds very little to anyone's understanding), and the cost of solving the problem is extremely large. I know a lot of AI people are effective altruists, but before they could smell the IPO money I didn't see any of them talking about how if they had $20 million the most effective thing they could do with it is spend it in an extremely environmentally costly way in order to prove Navier-Stokes. Back before AI I seem to remember these folks talking about like... mosquito nets and malaria treatments?
Mathematics is getting solved by AI. And this is a good thing.
why is that a concern in this context? would you have asked the same about steam engines and horses?
this is a really cool concept, organized very well. and that is very commendable.
So the issue isn't so much that LLMs will replace mathematicians, but that AI companies bragging constantly about how their machines "solve math" will convince people who don't understand the value of math research to no longer fund it, or students who don't yet understand why learning math is useful for developing their brains that it's a waste of time. That could put mathematicians out of a job without providing a useful replacement.
Motto: a mathematician's job isn't to solve the Hodge conjecture, it's to understand why the Hodge conjecture is or isn't true, and turn that understanding into something that makes it easier for the next person to grasp/use/enjoy.
LLMs absolutely have the potential to make this job easier, but the way in which these companies are using them right now risks being antithetical to that goal.
do you mean,
> All things AI seems to assume that more and faster is better, but there is no justification of that assumption.
is good argument?
of course faster discovery without human in the loop is better. is that not what humans have been optimizing for the past few thousand years ? faster mobility, faster communication, faster medical recovery etc. everything modern civilization has to offer is because of a rush to get better and faster. for example, discovering penicillin 2 years early would've saved ~15 million people more.
why is that not worthy enough to pursue?
I suspect you will find there is less appetite at the funding level for this kind of thing though, because what your funders really care about is generating headlines in front of their IPOs, and this kind of thing wouldn't generate the same headlines. I would be pleasantly surprised to be proved wrong of course.
EDIT: A more cynical point that I should add - I also suspect your funders would have less appetite for this kind of marathon because LLMs don't seem to be very good at this yet, which kind of points to the whole problem: so far, LLMs seem good at producing Lean proofs but not very good at the rest, but that fact is being lost in the media narrative, and "the rest" is actually the part that matters.
Similarly, humans don't need to be involved in scientific advances to benefit. We just need an aligned AI to take over the scientific thought for us. AI is already better than all but the top tier of humans at doing mathematics, it's writing most of the posts on the front page of this website, and it's doing the bulk of programming at many startups.
We can't put this genie back in the bottle.
If people are just doing math to kill time, I don't get why anyone would bother with AI. Do people really enjoy picking through a million lines of generated Lean code, if it's not for any practical use?
Maybe there's two kinds of math that we need? Useful math and navel gazing, and we can hand the first to the machines, and let hobbyists do the second in their free to entertain themselves?
Humans can try to extract some ideas from the million line lean proofs, if they want to, I guess. But I can't imagine anyone really funding the human part of it.
I agree with you on this point in isolation, but I think it's missing an enormous amount of context. Humans can absolutely benefit from science they weren't involved in and don't understand - I have no idea what a "histimine" is but I benefit from my allergy medication in the springtime.
That said, we're already living through a time where, on the whole, measures of intelligence, literacy, critical thinking, etc. are falling (at least in the US). That is a problem, which risks being exacerbated by AI, and the broader point is that we should be figuring out how to use these tools to produce knowledge that benefits humanity while also maintaining incentives for people to use their brains. Going back to my allergies: while I don't understand how my allergy meds work, my life is better, and I'm a better spouse/parent/friend/citizen etc., because I've taken the time to understand how other parts of the scientific and mathematical world that do interest me work. The current AI push to just throw out LLM-generated Lean proofs of everything under the sun to get headlines and pump up their IPO valuations (which this Marathon seems, intentionally or not, to be participating in), doesn't appear to be considering this alignment between what we get from AIs and how we can maintain our incentives to do human science. It seems more like measuring you-know-whats while risking that the message the broader public takes away is that math "has been automated" so what's the point in using your brain anymore?