Reseña: Numerical analysis of ordinary differential equations in Isabelle/HOL
El miércoles (15 de agosto de 2012) se presentó en el ITP 2012 (Interactive Theorem Proving) un trabajo de razonamiento formalizado en Isabelle/HOL titulado Numerical analysis of ordinary differential equations in Isabelle/HOL
Sus autores son Fabian Immler y Johannes Hölzl (de la Technische Universität München).
El resumen del trabajo es
Many ordinary differential equations (ODEs) do not have a closed solution, therefore approximating them is an important problem in numerical analysis. This work formalizes a method to approximate solutions of ODEs in Isabelle/HOL.
We formalize initial value problems (IVPs) of ODEs and prove the existence of a unique solution, i.e. the Picard-Lindelöf theorem. We introduce generic one-step methods for numerical approximation of the solution and provide an analysis regarding the local and global error of one-step methods.
We give an executable specification of the Euler method as an instance of one-step methods. With user-supplied proofs for bounds of the differential equation we can prove an explicit bound for the global error. We use arbitrary-precision floating-point numbers and also handle rounding errors when we truncate the numbers for efficiency reasons.
El código de la formalización en Isabelle/HOL se encuentra aquí.
. First we will state properties of vector spaces independently of their dimension. Then, we will introduce the conditions to obtain finite-dimensional vector spaces. The notions of linear dependence and independence, as well as linear combinations, and hence the notion of basis will be presented. Some results about the dimension of the different basis of a vector space will be necessary, as well as on the isomorphism among vector spaces. Once we have introduced the notion of basis, and with the additional condition of it being finite, we will introduce the notion of finite-dimensional vector space. Next step is to introduce vector subspaces. We will pay attention to vector susbpaces generated by a given set of vectors and prove some of their properties. The notion of linear maps will be also required to define isomorphisms of vector spaces. Finally, we will prove that a vector space (over a field 
.