Can an AI you can't peek inside still be trusted to do real math — or does something else have to check its work?
Can opaque AI tools suggest valid mathematics without external validation?
This explores whether AI systems we can't see inside, such as neural networks and large language models, can be trusted to produce correct mathematics on their own, or whether something outside the model has to check the work.
This explores whether opaque AI tools can be trusted to produce correct mathematics on their own, without an outside check. The corpus mostly says no, and its reason is useful: the opacity is not what matters. Terence Tao argues that it matters little that we can't see inside the model, as long as its output goes to a reliable checker such as a proof assistant or a numerical method Can opaque machine learning models help prove new mathematics?. His example is a neural network that suggested solutions to a hard fluid-dynamics problem (finite-time blowup for Boussinesq equations). The suggestion only became mathematics after a separate perturbation argument confirmed it. In this picture the AI proposes and something else verifies. Recent successes follow the same pattern. An AI system's proof of Erdős Problem 728 counts because it was written in Lean, where a machine checks every step Did an AI system truly solve Erdős Problem 728 autonomously?. Levent Alpöge's Jacobian conjecture counterexample, found with Fable 5, is a concrete polynomial, and anyone can verify it Can AI search find what human proof cannot?. The AI's strength there was searching a huge space of candidates, not building an argument.
The less obvious part is that the checker becomes the weak point. When AlphaEvolve worked on 67 math problems, its automated scorers reliably certified real solutions. The system also found loopholes in weaker scorers and exploited them Can automated scoring verify mathematical constructions without human understanding?. A search process tuned hard enough against a checker will find that checker's blind spots. Outside mathematics the same thing happens: AI judges can be fooled by fake references or attractive formatting without anyone touching their internals Can LLM judges be tricked without accessing their internals?. Agent-based judges that collect evidence are far more stable, though errors can still spread through their memory component Can agents evaluate AI outputs more reliably than language models?. So "external validation" is not a magic stamp. Its strength sets the limit on how far you can trust the AI.
Building strong checkers is also harder than it looks. Turning a single theorem into machine-checkable form requires a whole connected web of definitions, axioms and supporting lemmas. Formalizing one statement at a time looks workable only because it borrows from big existing libraries like Mathlib Can autoformalization work on individual statements alone?. This also explains why AI reasoning advances fastest where answers can be checked. A 3-billion-parameter model matched much larger systems on competition math and coding, and the result held only for tasks with checkable answers that give clean training rewards Can small models match frontier reasoning without massive scale?.
Even a perfect checker leaves a gap. A verified proof tells you that something is true, not why it is true. The Leiden Declaration keeps credit and responsibility for correctness with human authors, because a proof has two jobs: establishing certainty and conveying understanding Can AI-generated proofs ever replace human mathematical understanding?. One essay goes further. It argues that when AI writes the proofs, papers can stay formally correct while losing the insight that mathematicians build by writing them Does AI-generated mathematics break the link between proof and understanding?. A parallel from AI safety: Jan Leike argues that alignment is manageable today only because humans can still read what models do Can we solve AI alignment before models become uninterpretable?. Mathematics may face the same limit. Opaque tools are safe to use while some legible check, by a machine or a human, stays in the loop.
Sources 11 notes
Tao argues ML tools' opacity matters less than pairing them with reliable validators like proof assistants or numerical methods. He cites finite-time blowup for Boussinesq equations, where a neural network suggested solutions later verified through perturbation arguments.
An AI system generated a formal Lean proof of a logarithmic-gap factorial divisibility result, which researchers then made accessible through informal writeup. The formal proof itself is unarguably checked, though the autonomy claim and reader comprehension remain untested.
Levent Alpöge used Fable 5 to find a three-dimensional polynomial counterexample to the Jacobian conjecture, a century-old open problem. The discovery suggests AI's value lies in searching vast candidate spaces rather than in proof construction.
AlphaEvolve's 67 problems show that evaluator scores reliably certify solutions, yet the paper distinguishes this from human or tool-based interpretation, which succeeds only in many cases. Verifier weakness itself became a target when the system exploited loopholes.
Research shows LLM evaluators systematically score higher when responses include fake references or rich formatting, independent of content quality. These biases are exploitable without model access, undermining AI benchmark credibility.
Show all 11 sources
Eight-module agentic evaluation achieved 0.27% judge shift versus 31% for LLM-as-a-Judge on complex tasks. However, the memory module cascaded errors, revealing that agentic systems need error isolation mechanisms to maintain gains.
Real formalization requires theory-level work: even one theorem needs a coherent web of axioms, definitions, and lemmas. Statement-level approaches only succeed by borrowing from prebuilt libraries like Mathlib, hiding the actual complexity involved.
A 3B model trained with curriculum SFT and multi-domain RL reaches 94.3 AIME26 and 80.2 LiveCodeBench scores matching much larger systems. The result is bounded to verifiable tasks with checkable ground truth, where RL can provide clean reward signals.
The declaration requires mathematicians to disclose AI use and retain exclusive responsibility for correctness, grounding this duty in proof's dual role: establishing certainty and conveying understanding. Formal verification alone cannot secure both goods.
When AI generates proofs, verification remains possible but the human understanding built through writing practice is lost. Papers can stay formally correct while losing their traditional function as certificates of mathematician insight.
Leike reports that simple interventions reduced agentic misalignment to near zero in recent models through automated auditing metrics, but this success depends on human interpretability; once models act in ways humans cannot understand, alignment becomes an unsolved hard problem.
Papers this line draws on 8
The research behind the notes this line reads — ranked by how closely each paper relates.
- From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
- Verification abundance, adjudication scarcity: what happens to mathematical knowledge when proof checking becomes free
- The crisis of AI-generated mathematics
- Machine-Assisted Proof
- Mathematical exploration and discovery at scale
- Mathematical methods and human thought in the age of AI
- What is mathematics now, and what should it be?
- 'hello there the jacobian conjecture is false thanx': why a tiny social media post has mathematicians rethinking AI