Neural networks find high-amplitude water-wave candidates, and interval arithmetic plus Lean turn the residual bound into a checkable statement
Physics-informed neural networks could previously show only small residuals at sampled points, not how large the error is over the continuous domain. This pipeline has a network search the Babenko equation in conformal coordinates for high-amplitude gravity–capillary waves, and staged neural corrections, Fourier projection and Newton polishing cut the maximum sampled residual by about seven orders of magnitude. The candidate is then frozen as an explicit trigonometric polynomial, interval arithmetic yields a rigorous uniform bound on the continuous residual, and Lean machine-checks the deductions from that numerical bound to the final residual theorem.