Holger Thies: Towards certified ODE solving in Rocq

Note: we meet in classroom P.01

Holger Thies (Kyoto University)

Abtract: I present a formalization of a rigorous method for solving initial value problems for ordinary differential equations in the Rocq proof assistant. The construction follows the classical proof of the Cauchy-Kovalevskaya theorem, computing the Taylor series expansion of the solution by iteratively deriving its coefficients. The development is carried out over an abstract interface for exact real computation, which can, for example, be instantiated with the constructive real numbers of the Rocq standard library. I also present a more efficient instantiation based on the Rocq interval package.

Reference: H. Thies, Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq, Proceedings of CPP 2026, pp. 29–44.