Comment by deanCommie | Hacker News Reader

Comment by deanCommie | Hacker News Reader

Parent Full thread

Even before AI we used to say if you write code that you only barely understand, then it will be to complicated to debug. (and/or maintain)

Mochizuki was still one human and it required legions of other humans to unpack and untangle to confirm that it didn't lead to anywhere in particular.

AI is now capable of constructions so complex that no human or human team can unpack. And its ability to increase that complexity is growing while our human ability is stagnant.

meta-AI analysis cannot help. We (software professionals who use AI regularly) already know that if you run into a situation where a Fable/Astra-generated analysis reaches the limits of our comprehension/complexity due to their subjectivity, throwing more AI at the problem doesn't always converge.

There are many reasons to feel optimistic about AI, and ultimately its general ability to help science and mathematics.

I see no reason to feel optimistic about the future of mathematics and AI based on the current path of frontier labs, unless the misalignment Tao is writing about can be reconciled.

> AI is now capable of constructions so complex that no human or human team can unpack.

How can we possibly know this when we haven't even seriously started on the endeavor of actively reverse engineering these AI-generated proofs? That's a proper job for human mathematicians, because the AIs themselves are demonstrably clueless about what steps in a proof are genuinely interesting and load-bearing from a human POV. This is evidence of a limitation in AIs' capabilities, not of any kind of misaligned behavior. The fact that Tao actually uses that term in his complaint is deeply disappointing.

Not to mention, there are already (pre AI) machine-generated proofs that we've pretty much agreed not to try to explain fully, like the four-color theorem which ends up with brute-force verification of 600+ cases (down from close to 2,000 when first demonstrated)

> there are already (pre AI) machine-generated proofs that we've pretty much agreed not to try to explain fully, like the four-color theorem

Algorithmic verification is a very unsatisfying answer to the problem (e.g., surely it's not just dumb luck that every single case happen to have this exact property), but that's an entirely different issue than saying that no one follows logic of the proof method itself.

For the interested; the saying I believe you are referencing in regards to writing code / debugging is from Brian Kernighan, specifically:

  Everyone knows that debugging is twice as hard as writing a program in the first place. So if you're as clever as you can be when you write it, how will you ever debug it?

(from, 'The Elements of Programming Style')

It's prescient.

It’s a cute statement, but it doesn’t really match reality. Programs written by humans can generally be debugged by humans.

Could AI write programs that humans can’t understand or debug? Probably, but that’s not what Kernighan was describing.

> AI is now capable of constructions so complex that no human or human team can unpack

Can you give an example of this?

The first major computer-assisted proof, of the four-color map theorem in 1976, was an example of this. It created a lot of controversy at the time. It used proof by exhaustion, i.e. essentially analyzing every possible relevant case, something that no human could do without the assistance of, at the time, a supercomputer.

Reply on news.ycombinator.com