undefined

points

[-]

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

by kfse4 hours ago|

parent|

[-]

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)

by 12_throw_away3 hours ago|

parent|

[-]

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

by mk_stjames6 hours ago|

prev|

[-]

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.

by antonvs4 hours ago|

parent|

[-]

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.

by overfeed6 hours ago|

prev|

[-]

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

Can you give an example of this?

by antonvs4 hours ago|

parent|

[-]

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.