Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Learn to formalize a solver for initial value problems involving systems of multivariate analytic ordinary differential equations using the Rocq proof assistant in this 22-minute conference presentation. Explore the construction following the classical proof of the Cauchy-Kovalevskaya theorem, which computes Taylor series expansions of solutions by iteratively deriving coefficients. Discover how the formalization proves convergence of computed Taylor series and provides explicit bounds on truncation error to ensure arbitrarily small errors. Examine an abstract framework using type classes and setoids that maintains flexibility and compatibility with different implementations rather than relying on concrete constructive reals implementations. Study the extension to a more efficient variant based on interval arithmetic and see practical applications through several illustrative examples. Gain insights into formal verification, computable analysis, constructive mathematics, and the intersection of mathematical theory with computational implementation in modern proof assistants.
