Human mathematicians are being outcounterexampled

The strongest reaction was not panic about mathematicians being obsolete. It was a sharper distinction between two jobs. One is search, where brute force plus good heuristics and enough compute can now beat human patience. The other is understanding, where people still want a reason the conjecture looked true, what structural feature failed, and what corrected theorem should replace it. Several comments pushed that a bare counterexample is an answer, but not yet a satisfying theory. In practice, counterexamples are still valuable because they stop wasted effort and often force a better statement. A second theme was that this result probably was not “someone typed a clever prompt into ChatGPT.” People pointed to decades of pre-LLM computer-assisted checking, the existing literature narrowing the search, and the likelihood of substantial human mathematical setup plus optimized code. A reproduced prompt looked generic enough to undermine the idea that the magic was all in prompt engineering, but commenters still saw the real system as a hybrid of mathematician judgment, language-model assistance, and serious compute. That framing carried over to formal methods. Several people said they would have loved Lean-backed checking in university because lecture notes and even theses often contain proof gaps, and machine formalization is already useful as a correctness filter even when it is a poor teaching medium. The emotional undercurrent was less about AI hype than about how brittle mathematical authority can be. Stories about flawed theses, incorrect corollaries in the literature, and careers damaged by advisor politics landed hard. In that light, AI help is appealing not just as a discovery engine but as a way to surface mistakes earlier and make “the proof is in the slides” less of a power move.