Headlines and inside stories: understanding and trust in AI for mathematics, science, and engineering

[This is a guest post by Tapio Schneider. This blog post was initially written in a different file format and converted using AI. — T.]

[This will be cross-posted on the CliMA blog.]

The apparent proof of finite-time blow-up of the forced Navier-Stokes equation, announced by OpenAI on September 8, has brought into focus a debate about the role of AI in mathematics. The proof was produced with a system of some 10,000 AI agents that explored many approaches in parallel; it was then formalized and verified in Lean. The formal verification supports its correctness, but mathematicians are still working to digest it. A proof settles the truth value of a statement, but Terry Tao and others have argued that this is only part of the point of proofs; the other part is to advance our conceptual understanding of “basic structures of shapes, numbers, and natural phenomena.” As Yehuda Rav put it a quarter-century ago, “theorems are the headlines, proofs are the inside story.” A proof that is correct but incomprehensible, or undigested by the mathematical community, gives us the headline without the story. The issue is not whether the prover is a human or a machine, but whether the reasoning advances our collective understanding of methods and structures, which can spur new thinking and further advances. As Timothy Gowers has noted, the inadequate AI-generated write-ups of proofs are likely a temporary annoyance.

I want to argue that the same point about understanding holds in the natural sciences and engineering, where it also has intrinsic value and, in addition, acquires instrumental value when predictions must be trusted before they can be verified empirically. One role of science is what ancient philosophers called episteme, roughly explanatory understanding; here, understanding is the goal itself. Another role is techne, roughly the craft of predicting and making: forecasting how natural or engineered systems will behave under circumstances not yet observed. Whether the two roles can be separated depends on how easily predictions can be checked. When they can, techne can stand on its own. A black-box AI weather prediction model can predict tomorrow’s weather, and we can trust it because its forecasts can be checked every day. Techne can then also serve episteme as an instrument. For example, AlphaFold predicts 3D protein structures without providing explanations. But its predictions can be checked against experimentally determined structures, and they have become invaluable for understanding how drugs bind to their targets. Episteme and techne become inseparable when predictions must be acted upon, and hence trusted, before they can be empirically verified, because verification is too slow, costly, or dangerous, as in projecting climate change decades ahead or designing an aircraft. In those cases, an auditable causal chain from assumptions and input data to the predicted outcomes is what makes predictions trustworthy, and this constrains how AI can be used.

The Navier-Stokes equation, which describes fluid flow, is a good example, as it is at the heart not only of a Millennium Prize problem but also of aircraft design and climate prediction. The claimed result says that a fluid starting from rest, driven by just the right smooth stirring, develops an infinite velocity spike in finite time while its total kinetic energy remains bounded; the forcing is constructed to sustain the collapse. (The unforced version of the problem, whether smooth solutions exist for all time without external forcing, remains open.) Despite the mathematical singularity, nothing infinite happens physically: the incompressible equation stops being valid once energy concentrates at very small scales, where compressibility and molecular effects take over, as has long been known. By contrast, in turbulence, viscosity dissipates energy at a small but finite scale (the Kolmogorov scale), and the continuum description is valid across all scales of motions. Therefore, the result says little about how we model, predict, and understand the physical phenomenon of turbulence, which is likewise a solution of the Navier-Stokes equation, and one that, unlike finite-time blow-up, is ubiquitously realized.

The Navier-Stokes equation governs the flow and turbulence that control lift and drag around an aircraft wing, cloud formation in the atmosphere, and mixing in the oceans. In both aircraft design and climate prediction, verification comes late or is difficult and expensive. An aircraft is flight-tested only after it is built; a projection of how extreme rainfall statistics intensify in the coming decades must inform stormwater infrastructure that is built now but will likely be put to the extreme test only decades later. Such predictions earn trust not by end-to-end verification but by being the output of an auditable chain stretching from inputs (design parameters, atmospheric composition) to outcomes, whose links have known limits of validity and can be tested individually. Computational fluid dynamics (CFD) solves the Navier-Stokes equation together with additional equations (e.g., for thermodynamics) numerically. Its numerical methods for the resolved scales are based on established theories of stability, consistency, and convergence, and its subgrid-scale models for unresolved turbulence rest on plausible assumptions of universality at small scales (e.g., local isotropy) that can be tested separately against high-resolution simulations or laboratory experiments with canonical flows. Understanding and auditability of the individual links are what allow the chain as a whole to be trusted beyond the distribution of large-scale cases already observed, such as the present climate or existing aircraft wing designs.

Contrast that with end-to-end AI methods for weather prediction. Daily empirical verifiability suffices to establish trust in their forecasts. However, they do not come with a stability, consistency, and convergence theory (no analog of von Neumann stability analysis or the Lax equivalence theorem has been established for them), and how an initial condition becomes a forecast is difficult to audit. This is inconsequential for forecasting a few days ahead, where the forecasts can be checked daily. But it does matter for climate projection, which is a different task: predicting how weather statistics change over decades in response to a forcing such as increased greenhouse gas concentrations. An end-to-end model can learn the day-to-day evolution of weather states in today’s climate, but it contains no pathway through which greenhouse gases alter this evolution; their concentrations are typically not among its inputs, and if they were, no observations exist to learn about the response. The causal chain from greenhouse gases to their effects on radiative transfer, temperature, and winds, represented in physics-based models through their equations, is absent. Additionally, such models do not enforce conservation laws, for example of energy, so long integrations can drift by accumulating errors (e.g., in temperature). We would not currently trust them to project how the climate system responds to previously unobserved changes in the concentration of greenhouse gases over decades. Nor would we trust an AI surrogate of CFD simulations to certify an aircraft of novel shape. AI surrogates are used to explore and narrow down design spaces quickly, but the final assessment returns to established CFD methods or wind tunnel experiments, whose errors are controlled and whose steps are auditable.

So how do we best use AI in cases where episteme and techne combine, where understanding is essential for trust because predictions are difficult to verify? An answer suggested by the preceding argument is to embed AI at the links in the chain where trust can be earned by empirical verification. Concretely, use AI inside auditable scaffolds, such as physical conservation laws. Then use numerical methods with controlled errors to solve, e.g., the Navier-Stokes equation on the resolved large scales, while learning closure models for the unresolved subgrid scales from data, where some universality assumptions are defensible and individually testable. The rationale, in the case of the climate system, is that the large scales are where climate change moves the system out of the current distribution, whereas small-scale physics obeys the same local laws in a warmer or colder climate as in today’s. For an aircraft wing of novel shape, similarly, the geometry may be new but the functional relation between larger-scale conditions and the small-scale turbulence around it is not. The scaffold thus guides the extrapolation on the basis of the known equations, rather than with end-to-end models tied to the data available today.

Closures must be learned as functions of the resolved state, and extrapolation problems may reappear if the conditions for which data are available do not span the range of conditions for which predictions are needed (e.g., the temperature and humidity regimes in which cloud turbulence has been sampled, or the pressure gradients along a wing of novel shape). This can be mitigated with established tools, such as local high-resolution simulations for offline calibration and uncertainty quantification. Climate models and CFD codes have been built from resolved dynamics with embedded closures for decades. AI now enables a wider and faster search. Neural network closures can be individually tested and, to some extent, interpreted. Symbolic regression, which learns equations by selecting terms from a dictionary, as in SINDy, can sometimes produce closures that are more easily interpretable. AI agents are beginning to run the closure search in a closed loop, proposing symbolic closures, testing them against high-resolution simulations, observations, or experiments, and revising them. When this is successful, the resulting closure can be audited and, after the fact, understood.

This closed loop is similar to how AI is used in mathematics. In both cases, a verifier is used for checking: Lean for proofs; high-resolution simulations, observations, or experiments for turbulence closures. In the case of mathematics, the checks are complete; in the case of turbulence closures, they are limited to the conditions covered, so trust is restricted to the tested conditions. AI can accelerate this program by searching a larger space of possible closures or proof strategies than can be explored by humans in the same time. Once candidates have passed the checks, they become new objects for human study. In this way, understanding (episteme) and prediction (techne) improve together and reinforce each other, with humans, for now, remaining essential for extracting understanding and building trust in the end result: for writing the story behind the headline.

I thank Thomas Müller for pointing me to the paper by Yehuda Rav, and Thomas and my CliMA colleagues for discussions of the topics here over several years. I used AI for copy-editing.