Can opaque machine learning models help prove new mathematics?

Tao grants the objection first. Learned models are "often opaque", so it is "difficult to extract from the model a human-understandable explanation of why the model made a particular prediction", and at first glance they seem "unsuited for research mathematics, where one desires both rigorous proof and intuitive understanding of the arguments." He still finds "recent promising use cases of a suitably chosen machine learning tool to produce, or at least suggest, new rigorous mathematics, particularly when combined with other, more reliable techniques that can validate the output of these tools." The example is finite-time blowup for the Boussinesq equations. Wang, Lai, Gómez-Serrano and Buckmaster (2019) trained a Physics Informed Neural Network to produce approximate solutions, and a perturbation argument can then turn an approximate solution into an exact one. Tao presents this as complementary, not finished: a contemporaneous work by Chen and Hou established blowup for this equation with traditional numerical methods.

The mechanism is a division of labor between tools that fail in different ways. Tao's concern is that language models "hallucinate" plausible-looking nonsense, while a proof assistant's output is checked, since "the overall code only compiles if the proof is valid." Proof assistants can filter model output, and models could in turn "automate the more tedious aspects of proof formalization." His history shows why checking matters. The 1976 Appel–Haken four-color proof rested on a hand-checked calculation that "ended up containing multiple (fixable) errors", and the 1994 Robertson, Sanders, Seymour and Thomas argument, with 633 graphs, was built to be checked by code. Formalization remains slow: the "obvious" parts of an argument "can often take longer to formalize than the 'important' parts", because identifying (A1 × A2) × A3 with A1 × (A2 × A3) must be proved rather than assumed.

Against the nearest notes, Tao's version of opacity is the worry that Do foundation models learn world models or task-specific shortcuts? makes concrete: a predictor can be accurate without holding the structure behind its predictions. Tao's remedy in this excerpt is validation of the output, not explanation of the model. That is the asymmetry What limits how much models can improve themselves? formalizes for self-improvement, applied here to proof: a generator of candidate structures paired with a checker that does not share its failure modes. The contrast is with Can AI systems improve themselves through trial and error?, which validates by benchmark score rather than by formal proof or rigorous numerics. What counts as validated depends on the validator.

The excerpt does not establish that any of these pairings has yet produced a new theorem. Tao says "many of these combinations are still only at the proof-of-concept stage of development," and the blowup example reports a proposal and a parallel result, not a finished machine-generated proof. It also does not establish that validation yields understanding. Tao calls the Hales and Ferguson Kepler proof (1998) "very complicated (and computer-assisted)" and says nothing about whether anyone grasps why it holds. At the strength the evidence allows, a learned model's output can count as rigorous mathematics once an independent checker has passed it, and nothing in the excerpt says more than that about what mathematicians come to understand.