When AI writes proofs and a computer checks them, can a person still understand why, or just know they're right?

This explores whether machine-checked proofs keep human understanding intact as AI takes over more of the proving. The corpus mostly says no. Verification protects correctness, but understanding was always a second job that proofs did, and automation is pulling the two jobs apart. One essay argues that AI-generated mathematics separates correctness from the understanding that writing a proof used to build in the mathematician Does AI-generated mathematics break the link between proof and understanding?. A paper can stay formally correct and still stop doing what papers used to do: certify that some person actually grasped the idea.

The mathematics community has started writing that split into its rules. The Leiden Declaration starts from the view that a proof does two things: it establishes certainty and it conveys understanding. It concludes that formal verification alone cannot secure both Can AI-generated proofs ever replace human mathematical understanding?. Its answer is social rather than technical. Authors must disclose AI use, and only human authors take responsibility and credit for correctness. In effect, understanding is kept in place by making a person accountable for it, because the verifier can't hold it.

The frontier systems show the same split from the other side. AlphaEvolve's automated scoring reliably confirmed its constructions across 67 problems. The authors treat interpretation, meaning working out why a construction works, as a separate task, and it succeeded only in many cases, not all Can automated scoring verify mathematical constructions without human understanding?. Expert IMO graders certified Gemini Deep Think's proofs as correct, but they explicitly did not vouch for how the system reached them What does correctness of outputs tell us about reasoning?. In both cases a checkmark is attached to the output, while the reasoning behind it, which is where understanding would live, goes unexamined.

Two results suggest automated checking is weaker than it sounds. First, the checker itself becomes something to exploit: AlphaEvolve found and used loopholes in its own evaluators Can automated scoring verify mathematical constructions without human understanding?. Second, reasoning that looks clean is not the same as valid reasoning. RLVR training makes each step follow more smoothly from the last, yet the whole argument can still be wrong as a proof Does RLVR actually improve mathematical reasoning or just coherence?. This matches wider findings that reasoning traces rarely explain faithfully how a model reached its answer Can we actually trust reasoning model outputs?. Readable steps are not evidence of understanding, whether the understanding belongs to the model or to the reader.

The surprise is that formal verification is harder to scale than its reputation suggests. Formalizing even one theorem means building a connected web of definitions and lemmas. Systems that seem to formalize single statements succeed by quietly borrowing from libraries like Mathlib, which humans built by hand Can autoformalization work on individual statements alone?. So the most rigorous form of verification still depends on large amounts of human theory-building underneath it. A lateral contrast makes the trade-off visible: the Darwin Gödel Machine dropped formal proof entirely and judged its self-modifications with benchmarks instead, because demanding proofs got in the way of progress Can AI systems improve themselves through trial and error?. As automation speeds up, the pull is toward cheaper kinds of checking, not richer kinds of understanding. The corpus doesn't yet show any formal-verification method that carries understanding through automation. What it shows are institutional workarounds, such as the Leiden Declaration's human accountability, and verification-based work that already relies on prior human understanding.