Human mathematicians are being outcounterexampled
AI systems are now helping to find counterexamples to long-standing mathematical conjectures, such as a recent refutation of the Jacobian conjecture, prompting debate over how transformative this really is. Commenters weigh the novelty of a general-purpose model doing advanced math alongside coding and writing against the heavy human guidance, prompt design, and verification still required. Many see computer-generated counterexamples as a valuable way to save human effort and refine theorems, while others focus on questions of understanding, aesthetics in proofs, and the future role of human mathematicians.
Scope of the AI Counterexample Result
- Thread centers on an LLM-assisted counterexample to the Jacobian conjecture (degree‑7, 3 variables, 2026).
- Some argue this is not fundamentally new: computers have been used for counterexample search for decades; with enough tricks and compute, pre‑LLM systems might have reached similar examples.
- Others say the key novelty is that the same general-purpose model can do advanced math, code, write, and reason, instead of being a narrow expert system.
How Much Was AI vs Human?
- Emphasis that mathematicians still chose the problem, formalized it, and engineered the search; the prompt used in a reproduction is generic but nontrivial.
- Skeptics stress heavy human steering, long code runs, and proof checking; warn against overhyping “AI solved X” headlines.
- Supporters counter that this is exactly how humans collaborate, and that models can now autonomously design non‑naive searches over vast spaces.
Training and Generality of LLMs
- Debate over whether models are “trained on each task individually.”
- One side: classical AI required separate architectures and datasets per task.
- Other side: modern LLMs are trained with a single next‑token objective on diverse data, with RL surfacing capabilities; task performance emerges rather than being separately trained.
What Counterexamples Mean in Mathematics
- Many note counterexamples are central: they refine conjectures, sharpen theorem statements, and populate “bestiaries” of pathological cases.
- Some find counterexamples unsatisfying when they don’t explain why intuition failed; they want structural insight, not just a refutation.
- Others argue discovering any decisive counterexample is already highly valuable, especially for long‑standing conjectures.
Formalization, Proof Checking, and Error
- Discussion of Lean and other proof assistants: AI can generate massive formal proofs; humans may only need to understand definitions and theorem chains, not every lemma.
- Concern that math is already full of unnoticed errors; formalization projects aim to gradually verify the corpus.
- Worry about a future flood of AI‑generated “proofs” that humans can’t realistically check without mechanized verification.
Broader Impacts, Access, and Ethics
- Speculation that similar methods will hit other deep conjectures, then theoretical physics and CS, especially where verification is cheap.
- Some view paid access to strong models as a rational investment for grad students; others reject LLM use on ethical (data, environment) or intellectual grounds.
- Optimistic view: AI + humans as a “good team,” enabling outsiders with good models to collaborate meaningfully with under‑resourced researchers.