Scott Aaronson writes about OpenAI’s release of hundreds of AI-generated mathematical preprints, including a claimed proof of the Unique Games Conjecture, which his wife, mathematician Dana Moshkovitz, has worked toward for years. He is impressed by the apparent breakthroughs, but says people have not yet understood most of the proofs. Some have a Lean certificate — a computer check of a formally written proof — while others do not.

The difficult part now is making sense of what’s been released:

  • Moshkovitz describes the Unique Games manuscript as confusing and hard to read without AI assistance. A correct-looking result still needs explanation.
  • Aaronson says researchers are already poring over the papers to understand their arguments and make them legible to others.
  • He contrasts a mass release of raw proofs with Anthropic’s reported approach of giving selected researchers time to write up an AI-assisted result. One creates a race to interpret; the other lets a lab choose the interpreters.

The question isn’t only whether a model can reach a result. It’s whether mathematicians can verify what was actually proved, learn the ideas behind it, and keep doing meaningful work in the process.

The 219-comment thread on Hacker News adds a sharper verification question than the essay settles.

What the thread adds

  • an0malous — asks whether a Lean proof might check while formalizing the wrong statement: “Couldn’t the Lean code just be formulated incorrectly?”
  • prof-dr-ir — distinguishes statements that are straightforward to inspect from those needing extensive checking, and notes that some releases have only difficult-to-read PDFs, with no Lean formalization yet.
  • dualvariable — links a paper arguing that automated translation from ordinary mathematical prose into Lean can mistranslate the claim. That is a challenge to investigate, not a finding that these particular results are wrong.
  • softwaredoug — argues that a proof also needs to be “well written and intuitive to the average practitioner”; soVeryTired counters that even a sloppy first proof is a major step.
  • hintymad — offers a less bleak picture: AI could take on searches through existing knowledge, leaving people more room to develop new structures and techniques.

The unanswered question

an0malous and dualvariable, in different ways, ask what independent review would establish that the machine-checked theorem is the one the prose claims to prove. The thread raises the issue; it does not resolve it.

HN handles are pseudonymous, comments have no public per-comment scores, and their order is HN’s ranking. This is a slice of the discussion, not a consensus.