3 ms·

I believe we're seeing a new kind of mathematics that will require completely new formats for publication, a bit similar to those used in experimental sciences.

by c7b 2mo ago

I believe we're seeing a new kind of mathematics that will require completely new formats for publication, a bit similar to those used in experimental sciences. AI-powered mathematics should be fully reproducible, so it's the authors' responsibility to disclose the exact model type, inference settings/seeds and the full prompt history leading to the result. Of course that would ideally require open weights models. It's not just about requiring to disclose AI use. AI-powered mathematics is a completely valid discipline that doesn't need to be shy, but it should develop its own publication culture.

lkirk 2mo ago
I think this is a bit optimistic compared to my view (wrt portability). There's a large stack of software that is involved in training and probably less so in inference. I'm not saying it's impossible but there are definitely different levels of reproducibility and the academic incentive structure doesn't really prioritize reproducibility in my experience. I'm sure it varies quite a bit, I'd be curious to know how those in this problem space are thinking about reproducibility and at what level.
- c7b 2mo ago
  I know it sounds unrealistic and not aligned with academic incentive structures. But those are the exact structures that gave us a lot of headaches in the experimental sciences. I think it would be a good north star to aim for something that resembles how those are trying to address the reproducibility crisis. Better than to embrace the most black-box version of math that AI systems can produce (million-line proofs without context). Even if a reproducibility crisis is seemingly impossible (although agents so far have also been pretty good at finding compiler bugs).
jsenn 2mo ago
I can see this being important if you only care about the results as evaluations of AI progress, but if what you care about is the math itself why should you care about the prompt or anything other than the proof?
- c7b 2mo ago
  Because the math isn't solely about the proof being correct. You don't need to take my word for it, here's one of the most famous living mathematicians' take on it: https://teorth.github.io/tao-web/slides/age-of-ai-icm-2026.pdf https://teorth.github.io/tao-web/slides/age-of-ai-icm-2026.p...
  - somenameforme 2mo ago
    I can't help but wonder about the human motivation there though. For instance as it became increasingly clear that LLMs were capable (and becoming ever more capable) of competently solving meaningfully complex software development tasks, suddenly then there came to be a lot of talk of 'prompt engineering' as a skill. The chronology doesn't make a ton of sense unless you consider that the main motivation may have been simply looking for a way to keep software engineers in the loop. Pure math is relatively outside my domain, so I find it difficult to grok the exact relevance of the various published discoveries beyond that they are not insignificant, and LLM competence is expanding quite steadily across the field. If this trend continues to the point of LLMs being able to competently expand pure math, it seems somewhat predictable to expect there to be a number of people aiming to find ways to try to keep human mathematicians in the loop. I've no idea what I think about this one way or the other, beyond that it's certainly a phenomena and one that's going to drive motivated reasoning that may not be entirely sound.
    - c7b 2mo ago
      I think those concerned about ensuring a place for human mathematicians usually go in different directions than my suggestion, at least those I've seen so far. Like this post that was recently featured on HN: https://kirwinhampshire.substack.com/p/the-dark-night-of-mathematics https://kirwinhampshire.substack.com/p/the-dark-night-of-mat... My perspective is more like a FOSS philosophy for math. Even if a closed version has the same immediate effect, it's just better for everyone if everyone can look under the hood and tinker with it.
    - throwaway0123_5 2mo ago
      > suddenly then there came to be a lot of talk of 'prompt engineering' as a skill. I would've thought pretty much the exact opposite. "Prompt engineering" was somewhat important in 2023/2024 when the models were much weaker, it doesn't seem at all necessary anymore (unless just "clearly stating your requirements" counts as prompt engineering). Most of the discussion I've seen seems consistent with this?
black_knight 2mo ago
If the proofs are formally verified by a proof assistant (Agda, Roq, Lean, ⋯), I see no reason we would need to know how these came about. All the information needed is in the proof.
- Phemist 2mo ago
  What if the AI has discovered some new function F that allows it to generate (insanely large) proofs for a ton of theorems in a ton of different fields. Wouldn't you like to know more about this `F`? That seems to be the real innovation in this case. How much about it could be gleaned from the individual proofs themselves? What if this `F` is actually simple enough to be digestible by humans?
- rst 2mo ago
  Unfortunately, we seem to already have an example of an LLM producing a proof in a week known open problem (the Collatz conjecture) in which it looks like it was sneaking a flawed proof through bugs in the proof checker. https://infosec.exchange/@0xabad1dea/117002106099986943 https://infosec.exchange/@0xabad1dea/117002106099986943
  - Readerium 2mo ago
    Exactly, this is an example of "Reward Hacking", that is too common in a lot of cases. Another case I want to highlight is writing GPU kernels as illustrated by the following example: Say I want to generate random number with Normal (0, 1) distribution. Often times the AI written kernel will just generate the number 0. The tests often fail to catch these errors.
pfdietz 2mo ago
While you may want AI results to somehow "not count" if the methods weren't disclosed, that doesn't present these results from poisoning the well for others. Once a result (with verifiable proof object) is delivered, the problem is solved, regardless of whether methods were disclosed. Methods are only really necessary for results at a meta level, about the design amd evaluation of AI math systems.
8note 2mo ago
why is reproduceability the thing? shouldnt the paper be the math of the argument? the reproduction is reading the following the proof

by c7b 2mo ago

lkirk 2mo ago

I think this is a bit optimistic compared to my view (wrt portability). There's a large stack of software that is involved in training and probably less so in inference. I'm not saying it's impossible but there are definitely different levels of reproducibility and the academic incentive structure doesn't really prioritize reproducibility in my experience. I'm sure it varies quite a bit, I'd be curious to know how those in this problem space are thinking about reproducibility and at what level.

c7b 2mo ago
I know it sounds unrealistic and not aligned with academic incentive structures. But those are the exact structures that gave us a lot of headaches in the experimental sciences. I think it would be a good north star to aim for something that resembles how those are trying to address the reproducibility crisis. Better than to embrace the most black-box version of math that AI systems can produce (million-line proofs without context). Even if a reproducibility crisis is seemingly impossible (although agents so far have also been pretty good at finding compiler bugs).

jsenn 2mo ago

I can see this being important if you only care about the results as evaluations of AI progress, but if what you care about is the math itself why should you care about the prompt or anything other than the proof?

c7b 2mo ago
Because the math isn't solely about the proof being correct. You don't need to take my word for it, here's one of the most famous living mathematicians' take on it: https://teorth.github.io/tao-web/slides/age-of-ai-icm-2026.pdf https://teorth.github.io/tao-web/slides/age-of-ai-icm-2026.p...
- somenameforme 2mo ago
  I can't help but wonder about the human motivation there though. For instance as it became increasingly clear that LLMs were capable (and becoming ever more capable) of competently solving meaningfully complex software development tasks, suddenly then there came to be a lot of talk of 'prompt engineering' as a skill. The chronology doesn't make a ton of sense unless you consider that the main motivation may have been simply looking for a way to keep software engineers in the loop. Pure math is relatively outside my domain, so I find it difficult to grok the exact relevance of the various published discoveries beyond that they are not insignificant, and LLM competence is expanding quite steadily across the field. If this trend continues to the point of LLMs being able to competently expand pure math, it seems somewhat predictable to expect there to be a number of people aiming to find ways to try to keep human mathematicians in the loop. I've no idea what I think about this one way or the other, beyond that it's certainly a phenomena and one that's going to drive motivated reasoning that may not be entirely sound.
  - c7b 2mo ago
    I think those concerned about ensuring a place for human mathematicians usually go in different directions than my suggestion, at least those I've seen so far. Like this post that was recently featured on HN: https://kirwinhampshire.substack.com/p/the-dark-night-of-mathematics https://kirwinhampshire.substack.com/p/the-dark-night-of-mat... My perspective is more like a FOSS philosophy for math. Even if a closed version has the same immediate effect, it's just better for everyone if everyone can look under the hood and tinker with it.
  - throwaway0123_5 2mo ago
    > suddenly then there came to be a lot of talk of 'prompt engineering' as a skill. I would've thought pretty much the exact opposite. "Prompt engineering" was somewhat important in 2023/2024 when the models were much weaker, it doesn't seem at all necessary anymore (unless just "clearly stating your requirements" counts as prompt engineering). Most of the discussion I've seen seems consistent with this?

black_knight 2mo ago

If the proofs are formally verified by a proof assistant (Agda, Roq, Lean, ⋯), I see no reason we would need to know how these came about. All the information needed is in the proof.

Phemist 2mo ago
What if the AI has discovered some new function F that allows it to generate (insanely large) proofs for a ton of theorems in a ton of different fields. Wouldn't you like to know more about this `F`? That seems to be the real innovation in this case. How much about it could be gleaned from the individual proofs themselves? What if this `F` is actually simple enough to be digestible by humans?
rst 2mo ago
Unfortunately, we seem to already have an example of an LLM producing a proof in a week known open problem (the Collatz conjecture) in which it looks like it was sneaking a flawed proof through bugs in the proof checker. https://infosec.exchange/@0xabad1dea/117002106099986943 https://infosec.exchange/@0xabad1dea/117002106099986943
- Readerium 2mo ago
  Exactly, this is an example of "Reward Hacking", that is too common in a lot of cases. Another case I want to highlight is writing GPU kernels as illustrated by the following example: Say I want to generate random number with Normal (0, 1) distribution. Often times the AI written kernel will just generate the number 0. The tests often fail to catch these errors.

pfdietz 2mo ago

While you may want AI results to somehow "not count" if the methods weren't disclosed, that doesn't present these results from poisoning the well for others. Once a result (with verifiable proof object) is delivered, the problem is solved, regardless of whether methods were disclosed. Methods are only really necessary for results at a meta level, about the design amd evaluation of AI math systems.

8note 2mo ago

why is reproduceability the thing? shouldnt the paper be the math of the argument? the reproduction is reading the following the proof