Hacker News Reader

Comment by swiftcoder | Hacker News Reader

I've seen a lot of breathless reporting about various mathematical things being "proven" on the basis of the LLM-generated Lean formulation compiling. We probably wouldn't declare that for a human-written proof until peers had checked the proof for errors

View on HN

This. The proof of Fermat’s Last Theorem took 15+ months to check. It’s absurd to see the media reporting that these big problems are solved based off of a news release and a hastily and mostly AI-written manuscript, and OpenAI et al. are all too happy to run with said breathless reporting.

Wiles' proof was informal and couldn't be checked by a computer. In this case, the experts need to check 300 lines of Lean code (mostly comments) and confirm that it formalizes the problem statement correctly. There are papers building on the solution and analyzing it for more general versions of the problem, which suggests that the PDE community has already accepted it and moved on.

there's breathless reporting of just about everything scientific. physics, astronomy, archaeology, etc. have this sort of thing all the time.

yet i have never seen anyone say "the idea that physicists are beyond peer review is harmful" because some mainstream news articles published a piece about dark energy or whatever.

Exactly. Coverage here is "OpenAI has solved problem X", not "OpenAI has claimed to solve problem X."

Reply on news.ycombinator.com