Hacker News Reader

Comment by RunSet | Hacker News Reader

> Someone asked him what he thought of the AI proof. Justin said he didn’t know. He hadn’t read the paper yet. He said he’d been “too busy.”

> That astonished me. Too busy to look at a problem he had been dreaming about for 19 years? “I am genuinely busy and probably wouldn’t be able to get to reading a human’s proof immediately either,” he told me afterward, by email. “It does not help that AI does not write mathematics particularly well.”

Given:

* The human mathematicians can't solve the problems.

* The slop engine can't write well enough to make its purported solutions readable by human mathematicians.

* Sam Altman is a frivolous liar.

How is it possible to know whether the problems have been solved at all?

View on HN

Plain common sense. The same common sense that enabled people to discard the words of idiots on Reddit who claimed that ChatGPT was just Indians in a call center (a real talking point I ran into multiple times back then).

OpenAI does seem to be genuinely just high on their own supply for a little over a half of the manuscripts they released, but for the other half that is machine checked, either ((internal model)) managed to find a way to cheese 4 independent Lean checker kernels at the same time, and OpenAI somehow hasn't noticed / didn't report despite the heavy reputational risk, or the results are just plain correct. Go figure.

But even for the half that wasn't machine checked, there's an awfully big quiet regarding any defects in them. Given the insane schadenfreude potential and the highly potent David vs Goliat framing associated, one would expect any counterarguments to be frontpaged immediately, and be circlejerked to oblivion. Given that is yet to happen as well, go figure even harder.

Agreed. It's frustrating how everyone is pointing to the lean "proof", as if it's somehow irrefutable evidence that the problems have been solved.

Presumably with the level of interest in it people have been checking what the theorem definitions are to make sure they align and I would expect Anthropic to be burning a huge number of tokens to rip into the proofs and figure out if any of them are exploiting bugs in the lean kernel etc. at a point it's as close to irrefutable as you can get

Reply on news.ycombinator.com