Physicist Rikab Gambhir, writing a guest essay on Terence Tao’s blog, takes aim at AI-generated research that optimizes for output rather than understanding. This is satire: the supposed triumph of automating curiosity is the thing being criticized, not celebrated.

His argument has three parts:

  • Plausible-looking mathematical papers still need someone to establish what is correct and explain why it matters.
  • Gambhir argues that AI labs shift that checking and explanation work onto the research community while taking credit for generating results.
  • Treating science as a stockpile of answers loses something essential: people learning, creating, and understanding together.

The Library of Babel is his organizing metaphor: a collection containing every answer would not help much if nobody could distinguish insight from nonsense. The useful question is not simply how many papers an LLM can produce, but whether its use leaves people understanding more. This is a critique of incentives and claims about progress, not a technical audit of the generated mathematics.

The 134-comment thread on Hacker News adds a distinction between checking a proof and understanding it, plus counterexamples to the idea that AI necessarily displaces learning. Formal verification—software checking a proof against precisely stated rules—is one point of disagreement.

What the thread adds

  • mrob — “The whole point of formal verification is to remove the necessity of understanding most of the work. We only need to trust the formalization of the problem statement, the proof verifier, and the formalization of the result.”
  • joefourier — “Now with LLMs the process is much shorter. They can walk me through the algorithm step by step, translate it to pseudocode, explain equations, and most importantly, I can ask them questions and get clarifications, without worrying about seeming ignorant or exhausting their patience.”
  • user43928 — “I don’t see a convincing argument here that OpenAI does not in fact aim to further humanity’s understanding of mathematics, or that using AI for scientific discovery is comparable to automating away the fun parts of life.”
  • lacker — “So, which is going to be more useful - the sort of pure mathematics that AI does in 2026, or the sort of pure mathematics that humans do in 2026? That is the debate I would like to see.”

Passing that check does not itself supply a human explanation of the result’s significance. The disagreement here is useful: a tool that produces more unread work and a tool that helps someone understand a difficult paper can be the same technology, used toward different ends.

Handles are pseudonymous. HN publishes no per-comment scores; ordering is HN’s own ranking. This is a slice of the thread, not a consensus.