Neural Networks Solve Nonlinear Water Waves at Near-Machine Precision, Rigorously Verified with Lean

From Neural Network Discovery to Formal Verification: A New Paradigm for Nonlinear Water Wave Computation

Physics-informed neural networks (PINNs) show strong potential for solving partial differential equations, but their results often lack rigorous error guarantees. A recent study proposes a computational framework that combines machine learning discovery with computer-assisted numerical certification and formal verification. Targeting a strongly nonlinear PDE—periodic gravity-capillary waves—it achieves residuals at near-machine precision and provides auditable mathematical guarantees. This work not only demonstrates the neural network's ability to solve problems at high precision in the strongly nonlinear regime, but also explores a viable path of "AI discovery + rigorous proof."

Core Method: Staged Training and Data-Free Learning

The research team uses a physics-informed neural network as a search mechanism, learning the wave profile, wave speed, and—in continuation experiments—the surface tension directly from the governing equations, without any training data. Through a staged training and refinement process, the network achieves near-machine-precision equation residuals even in the strongly nonlinear regime. Interestingly, a single formulation recovers high-amplitude Stokes waves, Crapper waves, and Wilton ripples, demonstrating the framework's generality.

Starting from high-amplitude Wilton ripples and performing continuation in the surface tension dimension, the study also discovers new high-amplitude candidate solutions. These solutions do not appear out of thin air; they are a natural product of equation search and provide material for subsequent rigorous certification.

Physics-informed neural networks (PINNs) are a class of neural networks that embed governing equations as soft constraints in the loss function: the network takes spatial coordinates as input and directly outputs physical fields such as wave surface height. The loss terms include both the equation residual (e.g., how well the nonlinear water wave equation is satisfied) and boundary or periodicity conditions. Unlike supervised learning that relies on labeled data, PINNs use automatic differentiation to compute derivatives of various orders in the equation exactly, so they can "learn" the physical field without any numerical solution samples. In this work, this data-free property is particularly crucial—because high-amplitude strongly nonlinear waves have no ready-made analytical solutions, and traditional numerical methods struggle to converge stably, the network can only obtain supervision signals from the equations themselves. For this reason, the PINN here acts as a "candidate solution generator" rather than the final answer; its output must undergo independent a posteriori certification.

The periodic gravity-capillary waves in the paper refer to periodic traveling waves driven by both gravity and surface tension, whose governing equations contain nonlinear terms and higher-order dispersion terms. Surface tension significantly alters short-wave behavior and causes wave speed to vary non-monotonically with amplitude; in the high-amplitude regime, classical perturbation theory (such as Stokes expansion) often fails, and even anomalous phenomena such as curvature singularities at wave crests (Wilton ripples) appear. Such problems have long relied on numerical continuation and asymptotic analysis, lacking rigorous error control, making them an ideal testbed for the "neural network discovery + formal certification" framework: the network searches for candidate waveforms in parameter space, while interval arithmetic and Lean confirm that the candidates indeed approximately satisfy the equations.

Rigorous Certification: Interval Arithmetic and Lean Formalization

The candidate solutions produced by the neural network require independent verification. The authors freeze one candidate solution, convert it into an explicit finite representation, and then use interval arithmetic to give rigorous uniform bounds on its equation residual. This process accounts for floating-point rounding, Fourier truncation, aliasing, and grid-to-continuum errors, thereby independently verifying the neural network's precision.

Furthermore, the research team formalized the certification argument in the Lean theorem prover, machine-checking the derivation from the certified numerical bounds to the residual theorem. Both the interval certification and the formalization were completed with the assistance of large language models, but the validity of the results is independent of the language models: the numerical bounds are rigorously enclosed by interval arithmetic, and the subsequent mathematical derivations are checked by the Lean kernel. This forms a complete pipeline from neural network discovery to rigorous numerical certification to machine-checked verification, with auditable guarantees at every step.

Interval arithmetic is a method that replaces individual floating-point numbers with "intervals formed by lower and upper bounds": every operation guarantees that the true result lies within the computed interval, thereby accumulating floating-point rounding, truncation, and other errors into a rigorous overall bound. In the paper, the candidate solution is represented as a finite Fourier series, with each coefficient assigned an interval containing its error; these are then substituted into the governing equations for interval operations. If the resulting residual interval is sufficiently small, it provides a rigorous guarantee of "to what extent the approximate solution satisfies the equations." This explains why certification must account for Fourier truncation error and aliasing: truncation turns the infinite series into finite terms, while aliasing arises from the folding of discrete sampling in the frequency domain. Both must be incorporated into the interval width; otherwise the certification bounds would not hold.

Lean is an interactive theorem prover whose kernel uses dependent type theory and accepts only proof terms that have undergone rigorous logical derivation; any assertion not checked by the kernel cannot pass. The researchers encode the "numerical bounds given by interval arithmetic" as propositions in Lean, then progressively prove that these bounds imply the final residual theorem; the kernel checks the proof script line by line, thereby transferring trust in numerical results to trust in proof logic. The value of this approach lies in eliminating the "trust chain gap": numerical programs may have flaws, and code generated by large language models may contain errors, but as long as the Lean kernel accepts the proof, the correctness of the conclusion depends only on the kernel—a small and trustworthy foundation.

Significance and Limitations: The Trust Boundary of AI-Assisted Proofs

The most striking aspect of this work is that it clearly delineates the role of AI in mathematical discovery and verification. Large language models can assist in developing certification and formalization code, but the ultimate correctness does not depend on the models themselves—interval arithmetic and the Lean kernel provide a foundation of trust independent of AI. This "AI proposes, mathematics proves" model offers an example for the reliable application of AI in scientific computing.

However, the method currently targets a specific class of periodic traveling wave problems, and generalization to more complex PDEs and higher-dimensional problems remains to be explored. In addition, formal verification requires substantial engineering effort involving collaboration between humans and AI, and the degree of automation still has room for improvement.

Future Outlook: From Water Waves to Broader Nonlinear Systems

The framework's modular design—neural network search, interval certification, formal verification—gives it the potential to migrate to other strongly nonlinear systems. As interval arithmetic tools and theorem prover ecosystems mature, and as large language models improve in formal code generation, we have reason to expect more "certifiable AI discoveries" to appear in fluid mechanics, materials science, and other fields. For researchers interested in AI for Science, this work provides a new approach that balances exploration efficiency and rigor.