Asaf Karagila studies the Axiom of Choice, a foundational rule in mathematics. His response to OpenAI’s claimed progress on a century-old problem is not a verdict that the result is false. It is a complaint about what AI-generated research asks other people to do before it becomes useful.

  • He found the written preprint unclear in its structure, terminology, and references—even in his own specialty.
  • He did not review the accompanying Lean code, a machine-checkable representation of a mathematical proof. His criticism concerns the written explanation, not an audit of that code.
  • He argues that releasing hundreds of hard-to-read results shifts the cost of understanding them onto researchers with existing work and students to supervise.
  • He wants the community to establish standards for AI contributions, including whether reviewers should have access to the chat logs behind a paper.

The sharpest point is about responsibility: generating an artifact is not the same as communicating a contribution. Karagila argues that AI companies should meet the field’s standards rather than expect the field to reorganize around their output. That is the familiar AI-review bottleneck, with mathematical research rather than a pull request on the receiving end.

The 258-comment thread on Hacker News adds a software-support parallel and disagreement about whether difficult explanations justify setting the results aside.

What the thread adds

  • heyitsdaad — “It is along the lines of the fury I get when I am confronted with an 11 page dump of an issue analysis created by an AI agent that makes no sense but I have to go through because customer shared it.”
  • pelican0 — “But there are still diamonds (in the rough) in this drop that perhaps should be looked into. If the author is too busy, perhaps one of their students can take a look? Someone will, eventually.”
  • Athanase000 — “But I disagree that this low-quality writing is somehow a good reason to be angry at OpenAI specifically, otherwise you would have to be angry at a lot of people.”

The question the essay leaves open

Karagila does not establish whether the formal proof proves the intended claim. Two commenters approach that gap from different directions:

  • mcshicks — “Or you are saying you doubt the validity of the formal proof, which would also be interesting.”
  • stpedgwdgfhgdd — “Do you rely on the tests/Lean to accept correctness or not…”

A note on the discussion: handles are pseudonymous, HN publishes no per-comment scores, and ordering is HN’s own ranking. This is a slice of the thread, not a consensus; the excerpts above are commenters’ views, not verified findings about the proof.