logoalt Hacker News

hodgehog11today at 1:52 AM2 repliesview on HN

Why would they send it out for "expert review"? Every time, they have just made the AI generate a Lean proof. In fact, it seems like the most plausible direction to NS is computationally assisted detection of a blowup solution, which has fantastic automatic validation.


Replies

levocardiatoday at 5:03 AM

Anthropic sent out its Fermat's Last Theorem result to an expert on formalizing Fermat's Last Theorem in Lean, for what that's worth.

lumosttoday at 2:56 AM

How do you know the lean is correct? You don’t bet the two trillion dollar company on “the ai said so”

show 4 replies