The Evolution of Computer-Assisted Proof In Analysis

Abstract

The intersection of numerical analysis and machine learning, particularly in the domain of Neural ODEs and Physics-Informed Neural Networks (PINNs), relies heavily on discrete approximations of continuous flows. However, in stiff systems, explicit discretization schemes can induce topological bifurcations, creating spurious attractors that do not exist in the underlying continuous dynamics. In this paper, we analyze a stiff 2D nonlinear system integrated via Heun's method, demonstrating how the discrete map undergoes a numerical bifurcation that renders the true equilibrium repelling along an invariant manifold. Adopting a literate programming paradigm where "the paper is the proof," we embed a Computer-Assisted Proof (CAP) directly within the manuscript. Utilizing rigorous complex interval arithmetic and a dimensionality-reducing "Snap-to-Axis" projection, we mathematically verify that a neighborhood of trajectories is permanently captured by a spurious period-4 sink. This work highlights the critical need for formal safety certifications in learned dynamical models and provides a framework for verifying their stability.