4 ms·

Different person here, I read the article and they are all wrong. Hope that helps. Okay, to elaborate, substantively, their point is that the people using thes

Different person here, I read the article and they are all wrong. Hope that helps. Okay, to elaborate, substantively, their point is that the people using these AI models are not doing it for the love of the game, but for marketing. And instead of them - and nobody - spending millions of dollars to solve the problem, successfully, they want every problem of their academic industry to persist because even though they never solve the problem, they synthesize and solve lots of other problems nobody asked for. And get to boost their egos? Yeah, stop that. Actual alignment is on the humans themselves, if they want to remain relevant as academics and mathematicians, they need to learn how to replicate the proofs and the steps that alluded humans for decades and don't worry about the narcissistic elements that slow their industry down.

SpicyLemonZest 23d ago
Their claim is only indirectly related to the motivations of the people using their models. What they're saying is that doing math in this way does not produce the same value as traditional mathematical research, and the people using these AI models aren't concerned about that because their marketing objectives don't depend on whether their results produce mathematical value. If people doing valuable work are made irrelevant by people doing a larger volume of non-valuable work, that's not a positive outcome.
- deleted 23d ago
  [deleted]
- ndriscoll 23d ago
  But it does produce value. We now have an explicit solution and even a proof. Humans can then work on clarifying why it's true. Unsurprisingly, not all that different from software, where models can generate working code just fine. The details will all be there and all correct, but the architecture is currently not ideal, so a human guiding it can greatly improve the proofs. I actually found this to be the case with some basic linear algebra notes I was recently doing in Lean (without using mathlib). The model could generate working proofs, but they obscure the basic ideas (actually I wonder somewhat if this is because the Lean code that's out there to train on doesn't make a huge effort to read like textbook proofs, which was my motivation in the first place). I give it a skeleton of a couple lines of `calc`, letting it fill in the reasoning for each line, and it does much better. Then ask it about making some macros to simplify "trivial" or "obvious" things, and it does even better. etc. I suspect there's a good workflow where a big SOTA model makes an impenetrable proof (or code) and then a human works with a FIM model to simplify it (with the larger gnarly proof right there in context for FIM), but unfortunately everyone seems to only care about agents right now.
  - YeGoblynQueenne 23d ago
    >> Humans can then work on clarifying why it's true. Presumably you're a human. Are you going to do that?
    - ndriscoll 23d ago
      There are vanishingly few research mathematician positions and it's one of the most competitive fields, so no. But I'm not sure how that's relevant. As the OP says, usually the value of a proof is not the knowledge that something is true per se, but the reasoning techniques to understand why. How can it be anything other than helpful then to have a truth oracle as you try to figure out why things are true?
      - YeGoblynQueenne 22d ago
        So you're not going to do it yourself and you want someone else to do it for you? Some mathematician that dedicated their life to understand mathematics must now toil unpaid and unwillingly to understand the AI slop proofs that you want us to be able to understand? Do the job yourself. And if you can't, that's maybe a hint that you should listen to the people who can.
        ndriscoll 22d ago
        Who said anything about unpaid? I'm pretty sure professors don't show up just for fun. Our taxes pay them. I'd be happy to do the job. Actually I still dabble recreationally (clarifying Codex's Lean proofs, even!). But like I said it's one of the most competitive fields on the planet. As you say, you have to dedicate your life to it. If a slop proof isn't helpful, they don't have to "toil unwillingly to understand it". They can just proceed with the knowledge that the proposition they want to prove 1. is true and 2. is provable, which is already a decent start for motivation. But often LLMs can actually do quite well explaining ideas too in the hands of an expert. Or you can ask them to prove some technical lemma that you think ought to be true, and that could offer insight for the thing you're really interested in, but for which the details are actually not all that interesting to you. You don't have to one-shot "prove RH from the ground up in 50 million lines of Lean."
valegrete 23d ago
Mathematical breakthroughs with commercial relevance are few and far between, and often depend on dusting off old results which were, at the time of discovery, "solutions nobody asked for." The NS counterxample is actually, by any market measure, a "problem nobody asked for" in the sense that its existence doesn't have any commercial relevance (beyond juicing OpenAI's IPO). So the only long-term value solving it could have is by virtue of whatever reusable theory/insights were generated along the way to the counterexample itself. The letter is absolutely right on that point. It's not actually clear that those insights will come faster from reverse engineering this LLM proof vs. humans building theory to solve the problem themselves. So what you're saying may or may not even be an efficient way of operating. Also, it implicitly depends on mathematicians to do the hard work of creating problems and then deciphering LLM hieroglyphics for essentially free while the only immediately profitable component gets outsourced to a frontier lab. In what world is that model going to work? Reading between the lines, it seems like maybe you have a personal grudge for some reason and simply think the technology will advance enough to where we won't need academics at all. But you should say that in the first place.
- yieldcrv 22d ago
  What irks me is the ego My stance is that solving the problem is aligned with humankind the rest is just hypothesizing a way that academics fit in this world at all
  - valegrete 22d ago
    I just wonder whether a lot of smart people who never needed to go beyond the "solve for X" algorithmic math of a typical calculus sequence are actually reading the declaration the way the signatories wrote it. The Navier-Stokes problem is not exhausted by a simple 'no' counterexample (which most people familiar with the equations already expected to exist). In fact, I haven't heard a single person's explanation for what relevance this counterexample has for humankind. It is something impossible in our physical reality so we have gained zero insight into anything we actually model with NS. Mathematicians agree that "solving the problem is aligned with humankind." They disagree that releasing a counterexample this way actually constitutes "solving the problem" precisely because there is now little incentive to do the hard theory-building work that actually has the track record of leading to human advancement.
gjulianm 22d ago
> I read the article and they are all wrong I would recommend a bit more humility and trying to better understand why 25 Fields medalists, among them people like Terence Tao (who isn't anti-AI by any means, he's even promoted a registry of AI Lean proofs), are saying this. > Okay, to elaborate, substantively, their point is that the people using these AI models are not doing it for the love of the game, but for marketing. No. The point is that AI companies are using the models to solve problems in such a way that the useful part of problem-solving, i.e. the theories and tools developed during the process, is not present. And they are doing that because the companies seem to be motivated not by honest advancement of math but by marketing and publicity. > they synthesize and solve lots of other problems nobody asked for. No one asked Fourier to solve series representation of functions when he was studying the heat equation, and yet thanks to that we have Fourier analysis. > if they want to remain relevant as academics and mathematicians, they need to learn how to replicate the proofs and the steps that alluded humans for decades The point they are making is that if AI keeps being used as "problem solver" rather than "theory understanding", replicating the proofs and getting the useful parts out of them will be far more difficult.

SpicyLemonZest 23d ago

Their claim is only indirectly related to the motivations of the people using their models. What they're saying is that doing math in this way does not produce the same value as traditional mathematical research, and the people using these AI models aren't concerned about that because their marketing objectives don't depend on whether their results produce mathematical value. If people doing valuable work are made irrelevant by people doing a larger volume of non-valuable work, that's not a positive outcome.

deleted 23d ago
[deleted]
ndriscoll 23d ago
But it does produce value. We now have an explicit solution and even a proof. Humans can then work on clarifying why it's true. Unsurprisingly, not all that different from software, where models can generate working code just fine. The details will all be there and all correct, but the architecture is currently not ideal, so a human guiding it can greatly improve the proofs. I actually found this to be the case with some basic linear algebra notes I was recently doing in Lean (without using mathlib). The model could generate working proofs, but they obscure the basic ideas (actually I wonder somewhat if this is because the Lean code that's out there to train on doesn't make a huge effort to read like textbook proofs, which was my motivation in the first place). I give it a skeleton of a couple lines of `calc`, letting it fill in the reasoning for each line, and it does much better. Then ask it about making some macros to simplify "trivial" or "obvious" things, and it does even better. etc. I suspect there's a good workflow where a big SOTA model makes an impenetrable proof (or code) and then a human works with a FIM model to simplify it (with the larger gnarly proof right there in context for FIM), but unfortunately everyone seems to only care about agents right now.
- YeGoblynQueenne 23d ago
  >> Humans can then work on clarifying why it's true. Presumably you're a human. Are you going to do that?
  - ndriscoll 23d ago
    There are vanishingly few research mathematician positions and it's one of the most competitive fields, so no. But I'm not sure how that's relevant. As the OP says, usually the value of a proof is not the knowledge that something is true per se, but the reasoning techniques to understand why. How can it be anything other than helpful then to have a truth oracle as you try to figure out why things are true?
    - YeGoblynQueenne 22d ago
      So you're not going to do it yourself and you want someone else to do it for you? Some mathematician that dedicated their life to understand mathematics must now toil unpaid and unwillingly to understand the AI slop proofs that you want us to be able to understand? Do the job yourself. And if you can't, that's maybe a hint that you should listen to the people who can.
      - ndriscoll 22d ago
        Who said anything about unpaid? I'm pretty sure professors don't show up just for fun. Our taxes pay them. I'd be happy to do the job. Actually I still dabble recreationally (clarifying Codex's Lean proofs, even!). But like I said it's one of the most competitive fields on the planet. As you say, you have to dedicate your life to it. If a slop proof isn't helpful, they don't have to "toil unwillingly to understand it". They can just proceed with the knowledge that the proposition they want to prove 1. is true and 2. is provable, which is already a decent start for motivation. But often LLMs can actually do quite well explaining ideas too in the hands of an expert. Or you can ask them to prove some technical lemma that you think ought to be true, and that could offer insight for the thing you're really interested in, but for which the details are actually not all that interesting to you. You don't have to one-shot "prove RH from the ground up in 50 million lines of Lean."

valegrete 23d ago

Mathematical breakthroughs with commercial relevance are few and far between, and often depend on dusting off old results which were, at the time of discovery, "solutions nobody asked for." The NS counterxample is actually, by any market measure, a "problem nobody asked for" in the sense that its existence doesn't have any commercial relevance (beyond juicing OpenAI's IPO). So the only long-term value solving it could have is by virtue of whatever reusable theory/insights were generated along the way to the counterexample itself. The letter is absolutely right on that point. It's not actually clear that those insights will come faster from reverse engineering this LLM proof vs. humans building theory to solve the problem themselves. So what you're saying may or may not even be an efficient way of operating. Also, it implicitly depends on mathematicians to do the hard work of creating problems and then deciphering LLM hieroglyphics for essentially free while the only immediately profitable component gets outsourced to a frontier lab. In what world is that model going to work? Reading between the lines, it seems like maybe you have a personal grudge for some reason and simply think the technology will advance enough to where we won't need academics at all. But you should say that in the first place.

yieldcrv 22d ago
What irks me is the ego My stance is that solving the problem is aligned with humankind the rest is just hypothesizing a way that academics fit in this world at all
- valegrete 22d ago
  I just wonder whether a lot of smart people who never needed to go beyond the "solve for X" algorithmic math of a typical calculus sequence are actually reading the declaration the way the signatories wrote it. The Navier-Stokes problem is not exhausted by a simple 'no' counterexample (which most people familiar with the equations already expected to exist). In fact, I haven't heard a single person's explanation for what relevance this counterexample has for humankind. It is something impossible in our physical reality so we have gained zero insight into anything we actually model with NS. Mathematicians agree that "solving the problem is aligned with humankind." They disagree that releasing a counterexample this way actually constitutes "solving the problem" precisely because there is now little incentive to do the hard theory-building work that actually has the track record of leading to human advancement.

gjulianm 22d ago

> I read the article and they are all wrong I would recommend a bit more humility and trying to better understand why 25 Fields medalists, among them people like Terence Tao (who isn't anti-AI by any means, he's even promoted a registry of AI Lean proofs), are saying this. > Okay, to elaborate, substantively, their point is that the people using these AI models are not doing it for the love of the game, but for marketing. No. The point is that AI companies are using the models to solve problems in such a way that the useful part of problem-solving, i.e. the theories and tools developed during the process, is not present. And they are doing that because the companies seem to be motivated not by honest advancement of math but by marketing and publicity. > they synthesize and solve lots of other problems nobody asked for. No one asked Fourier to solve series representation of functions when he was studying the heat equation, and yet thanks to that we have Fourier analysis. > if they want to remain relevant as academics and mathematicians, they need to learn how to replicate the proofs and the steps that alluded humans for decades The point they are making is that if AI keeps being used as "problem solver" rather than "theory understanding", replicating the proofs and getting the useful parts out of them will be far more difficult.