alt Hacker NewsMost of the arguments here feel like gate keeping and resistance to change. I didn't see any arguments that were directly about advancing the state of knowledge of math.
“Current automated techniques can produce plausible but unreliable (or even incorrect) arguments which are difficult to distinguish from correct mathematical proofs.”
That seems like a problem for mathematics with or without AI.
Isn’t this a problem with human proofs as well?
“Many current models are also built on data obtained by systematically exploiting licenses and access arrangements that were not made with artificial intelligence in mind, or indeed by simply violating copyright protections”
Copyright? The copyright arguments have been hard to make in domains where copyright is much stronger, mathematical knowledge isn’t even subject to copyright.
“Technologies which affect the way in which mathematics is practiced may disturb the current system of incentives”
Resistance to change again.
“Proper evaluation is endangered if results are communicated through informal channels”
Gatekeeping again.
Replies
> Isn’t this a problem with human proofs as well?
Human proofs are themselves a kind of a proof of work. They certainly write flawed proofs, but you can expect a human author of a paper to have put in more effort--substantially more--than the human reader needs to verify it. Arguably, this asymmetry disappears for generated proofs.
Automated theorem provers help a bit here, but they don't eliminate the human verification cost.
You aren’t really engaging with the substance or heart of the post, and your reading feels a bit knee-jerky and bad-faith to me.
Can't all proofs be eventually broken down into their fundamental pieces and then it's clear as day if it's right or wrong? Seems like a proof would be the best place to determine if an AI is right or not because the output is either right or wrong, there's no subjectivity and the, now common, excuse "well a human would have done the same" won't hold up.
It is, but it is somewhat worse for machine-generated proofs, especially when the proof is very long and was done by brute force (eg the 4 colour map theorem[1] is the famous example), or depends on a lot of niche results in disparate areas (which LLMs are wont to sometimes do).
Even when the proof is produced by the llm in a formal system like Lean4 it may not be “honest”[2] and it can be hard to tell if the proof is very long and complex and especially if it includes highly specialized results from lots of different areas of maths. Llms can (and do) do this just fine, but for a human proof that would require a team each of which was specialized in a particular area. Those people are more likely to be able to cross-check each other.
[1] https://pubs.ams.org/ebooks/conm/098/ and https://en.wikipedia.org/wiki/Four_color_theorem
[2] An “honest” proof may contain bugs or errors but it does not constitute a deliberate attack on the proof system or the math libraries it uses. Systems like Lean aim to not incorrectly validate an honest proof with mistakes but don’t guarantee anything in the case of a proof being dishonest. This is the sense used here https://lean-lang.org/doc/reference/latest/ValidatingProofs/ .
Your list is cherry picked from the list of "potential threats" to the values of the mathematical research community identified by this document. They aren't criticisms or absolute statements, they're literally a list of potential new problems for the future of mathematical research, and they all seem reasonable to me, if not all at the same levels of magnitude or plausibility.
Notably you don't seem to be looking at either the list of identified values or their recommendations to researchers in their use of LLMs, which would seem much more important to engage with in any non-shallow dismissal of the document as "feel[ing] like gate keeping and resistance to change".
It's also kind of a bad look (and actively harmful for discourse) for people working on AI to be so dismissive of fields actively engaging with how their field is changing due to AI. I haven't seen any other field engaging this actively with its possible futures, have you? Usually we seem to only get some extreme of over-hyped utopia, doomerism, or dismissal of everything as slop.
There is some of that but I wouldn't call it gatekeeping. Universities lately promote citations and publications so there's a sense that results are all that matters. Results matter, yes, but there's a human side too where we're kind of asking about human creativity and ability. To me an appropriate analogy is in climbing Mt. Everest. Proving something, or even writing a thesis, is like climbing Mt. Everest. A lot of the value is actually in the effort you put into it. You could take a helicopter ride up to the top and then climb a few steps and claim "You climbed to the peak of Everest". That's like using AI. But if you asked them about what it was like, how they prepared, etc. their answer would not be helpful. So I think there is a lot of value in the journey itself and outsourcing all this to AI would destroy the human part of it.