The issue of credit is a relatively minor point in the declaration.
It's more about bypassing the culture and processes mathematicians have developed that lead to human understanding, generating new ideas, and bringing up new generations of mathematicians. (See also his article about "non-renewable mining" of good problems.)
Reducing mathematics to "let's just generate results through an isolated and automated system" is a misalignment since it bypasses those processes.
> The issue of credit is a relatively minor point in the declaration.
What a load of croc. This entire debate is fueled by a perceived lack of attribution. The AI learnt from researchers and did not give them a sporting chance of being first before scooping them. They were expecting some sort of fair play, instead they got a ruthless machine. Every other tangent to this debate is irrelevant, the culture, the community, the shared symbolic growth. Every mathematician I know is secretly trying to one-up their peers.
I wonder if this is a root of the complaints across fields, how AI is ruining the greater picture and process in writing, acting, drawing, filming, coding, and more.
That it makes life more ends and less means.
It's also known as "commodification of labour", and AI is just the latest and greatest tool to do it.
Luddites complained that the trajectory of technology was to allow less skilled workers to mass produce goods via machines owned by factory owners, as opposed to helping skilled workers build up and use their skills while passing them on.
Now we have a lot of money and time focused on LLMs owned by a few companies, making it easier for them to monetize low skill labour(prompting versus art/research/artisanry)
Let's take your argument one step further.
Suppose that tomorrow we learn that AI just exploited a bug in Lean and the proof is, in fact, bullshit. Or suppose it is the case, but we never learn that.
Where are "ends" and where are "means" here?
Well, given a proof of something then a system can be built that relies upon the inviolability of that thing.
Should the proof turn out to be bullshit, then that system will be revealed to be unreliable. Maybe.
I don't think it really attacks human understanding though. You can still read and understand an AI written proof. If another person comes up with a solution to a problem, you can read their methods and understand it. It doesn't matter if a human came up with that or not. It's really only attacking the "generating new ideas" part.
That's precisely the problem though. You cannot still read and understand an AI written proof at the current skill level of the AI being applied, because they're orders of magnitude longer than human written proofs even when they don't need to be, and spend most of that length on the parts that aren't important. This has been really thoroughly documented by expert mathematicians who are engaging with AI in public like Terence Tao and showing in detail how much work it takes working alongside AI to figure out how to understand AI generated proofs. With human generated proofs that process is forced to happen before publishing the proof because the new style of AI generated proofs validated only by formal verification is supplanting the old human peer review process that forced the burden of understanding onto the publisher and not the reader.
> You cannot still read and understand an AI written proof at the current skill level of the AI being applied, because they're orders of magnitude longer than human written proofs even when they don't need to be, and spend most of that length on the parts that aren't important.
Just like how they write software, then :-)
That doesn't seem to be true. The OpenAI NS paper was 166 pages. Wiles-Taylor proof of Fermat's last theorem is 129 pages. The length is not unprecedented for a difficult unsolved problem.
To be honest, I feel like the difficulty of reading AI proofs is due to the fact that we are on the verge of being beyond human comprehension. This is a demonstrable fact as no human has figured this out despite the problem being open for almost 100 years.
> To be honest, I feel like the difficulty of reading AI proofs is due to the fact that we are on the verge of being beyond human comprehension.
I can see where that's coming from, but I really don't think it's the case. Even with Astra, the proofs you get are just off in a way that doesn't signal superhuman comprehension. As 9question1 says, a common theme is that they dwell on insignificant steps. Another one is that they'll often be full of terminology that either doesn't exist, or has this weird quality where it looks like it is trying to make some minor insight seem much greater than it is. At first glance, that'll often make it look like it knows more than you, but when it's really just doing the same thing but in a more complicated and worse fashion, that to me isn't a signal of comprehension at all. The bizarre thing is that despite all the "stochastic parrot" style nonsense you'll get in individual proof steps, they still often combine to something valid.
In either case, what all of this means is that the working mathematician still needs to go through, and generally completely rewrite, any proof output by an LLM. Otherwise you are passing the burden of unreadability onto the reader.
Yeah, that mirrors what I've seen throwing some of the leading models at a set-theory problem that's stumped me (https://mathoverflow.net/q/511601): in this case, the problem does not easily yield to the standard tools, but the LLMs do not recognize it as a major open problem they should give up on. So they seriously try it, but typically end up in a loop of inventing certain classes of simple solution or counterexample attempts, defeating them, and trumpeting each one as a major result, each time inventing some new terminology.
It's definitely quite curious that the AI labs are able to push these results through seemingly with pure brute force. Perhaps it's largely a function of how many monkeys you have attempting various constructions on top of the known results and strategies the models have memorized.
That matches my experience with AI writing in software engineering so I’m not surprised
> This is a demonstrable fact as no human has figured this out despite the problem being open for almost 100 years.
That's not true. Alpoge and Buckmaster's related LLM-assisted blowup result (https://news.ycombinator.com/item?id=49605915) utilized a strategy developed recently by Cordoba and Martinez-Zoroa.
This is a very token-brained take. The length of a work has no bearing whatsoever on its comprehensibility.
Not "a" human's understanding; Humanity's understanding. Understanding the research problem, and the solution especially, is a lot more involved than simply "read their methods". That's the whole point being made.
It matters if a human came up with it because of everything mentioned in the article... A mathematician's solution is necessarily built on other's ideas that have been disseminated, internalized, pressure tested etc. Methodologies differ too. AI can abuse its compute resources and generate a true/false or counterexample statements, without laying the foundation that a decade of globalized research would have.
>You can still read and understand an AI written proof.
No you can't lol, they're multi million lines of Lean, which is already an obscure language to understand. It's an assault on your senses.
It's not only Lean code, there are English writeups too. To my understanding the pipeline for these problems is 1) solve in english 2) formalize systematically to check. No one is tackling problems purely in Lean, to my understanding.
https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8...
[dead]
I agree that the declaration doesn't focus on credit, but I think it's still at the root of the problem. Because ask yourself: if the AI generated proofs are not creating any new ideas or insight, just brute forcing a boolean true/false result, then why can't mathematicians simply ignore their results? Why does it matter if OpenAI or even amateurs with AI are "solving" these problems, without contributing to any deeper understanding?
I don't think "intellectual poisoning" is really the mechanism that harms the mathematics community.
The harm is if you have a community of mathematicians who are focused on expanding human understanding, then having instant access to a bunch of AI proved results muddies the water about who has contributed what. If someone could scoop any significant theorem at any time by pointing an AI at it, how do you really demonstrate that you have created new understanding? Or that your new understanding is about something important? How do you prove that the AI needed your new concepts to be able to solve it?