← Back to context

Comment by rtpg

11 hours ago

The problem is that one a person writes a 60 page proof in theory that person has spent an inordinate amount of time on the proof and can answer questions, describe some insight, etc etc.

If a random person is given a 60 page proof to digest and not the author, those hidden insights that _aren't_ in the paper might be completely inaccessible. Maybe the AI will "just" be able to provide the insights. Maybe. But pedagogy is tricky work, and despite these AIs being able to do all this fancy math we can't get them to write good cover letters yet, so....

Ultimately we might be left with just a bunch of intellectually unsatisfying proofs. This means way less drive to simplify the proofs or rework them.

End result: we generate a layer of "less efficient" mathematics, that won't get built upon. We will not actually have any shoulders upon which to stand.

AI can simplify and rework proofs too.

  • According to Scott Aaronsson, OpenAI set their agents on 8000 different problems, and got 372 final proofs. Even spending twice the original effort on simplifying and reworking those proofs so that they do not "feel like something written by someone who’s on psychedelics" would only increase the compute by less than 10% (assuming all the agents had a similar token budget).

    The fact that they did not do so can only mean that either (1) their agents currently lack the capability to do it, or (2) OpenAI are completely indifferent and do not care in the slightest if the proofs are understood or not.

    • > The fact that they did not do so can only mean that either (1) their agents currently lack the capability to do it, or (2) OpenAI are completely indifferent and do not care in the slightest if the proofs are understood or not.

      Come now, this is kind of unreasonable. When you're working on a new technology, you first get the ugly, inconvenient-to-use prototypes functioning with the core new thing you need; then you work on packaging it up into a format useable in production. I'm sure the very first digital camera sensors weren't very useful for photographers either; but it isn't really even possible to build the rest of the technology required to turn raw output of a digital sensor into something a professional photographer can use until you have the raw output itself.

      The research is still on going on the raw output; getting things to the next stage, where the results are widely useable by professional mathematicians (and then on to engineers and scientists to whom the results would be practically useful), is a whole new research area.

      3 replies →

But why should process of discovering mathematical insights be any less attainable to AI models?

The concern is being raised without evidence, because the evidence points to the gap simply being frontier models have just started to be able to get a raw proof out. Why, given existing progress, should we expect them to be unable to distill insights from those proofs?

Certainly this even more likely doesn't matter at all for applications: if I can send a radio signal further because my AIs design it a certain way, that's an unambiguous result. Which is really the next step here: turn a proof into a "mechanical" application.