3 ms·

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

by tmhn2 22d ago

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.

jimkleiber 22d ago
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.
- gritzko 22d ago
  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?
  - margalabargala 22d ago
    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.
- Xelynega 22d ago
  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)
  - int_19h 22d ago
    > 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. And their complaint was valid from their perspective, but the end result of that process is that now you can have functional and pretty clothing for pennies. It's true that a lion's share of the gain was pocketed by people who owned the mechanized looms. Now imagine how much more of an advantage it would have been without those people. Same thing here. We can - and should - get rid of all the megacorp leeches. But the benefits of cheap automation remain regardless, and it's still the same equation - removing the gatekeeping harms those who relied on it to keep the products of their labor priced high, while benefitting everyone else.
jrflo 22d ago
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.
- 9question1 22d ago
  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.
  - jrflo 22d ago
    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.
    - jscd 22d ago
      This is a very token-brained take. The length of a work has no bearing whatsoever on its comprehensibility.
    - pred_ 22d ago
      > 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.
jeremysalwen 22d ago
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?
glitchc 22d ago
> 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.

by tmhn2 22d ago

jimkleiber 22d ago

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.

gritzko 22d ago
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?
- margalabargala 22d ago
  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.
Xelynega 22d ago
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)
- int_19h 22d ago
  > 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. And their complaint was valid from their perspective, but the end result of that process is that now you can have functional and pretty clothing for pennies. It's true that a lion's share of the gain was pocketed by people who owned the mechanized looms. Now imagine how much more of an advantage it would have been without those people. Same thing here. We can - and should - get rid of all the megacorp leeches. But the benefits of cheap automation remain regardless, and it's still the same equation - removing the gatekeeping harms those who relied on it to keep the products of their labor priced high, while benefitting everyone else.

jrflo 22d ago

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.

9question1 22d ago
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.
- jrflo 22d ago
  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.
  - jscd 22d ago
    This is a very token-brained take. The length of a work has no bearing whatsoever on its comprehensibility.
  - pred_ 22d ago
    > 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.

jeremysalwen 22d ago

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?

glitchc 22d ago

> 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.