alt Hacker NewsAgreed. It's frustrating how everyone is pointing to the lean "proof", as if it's somehow irrefutable evidence that the problems have been solved.
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