Lorenz used a system of ordinary differential equations (ODEs) to study atmospheric dynamics phenomena [1]. He established the great sensitivity of the results obtained by this simplified model to very small, nearly negligible changes in the initial conditions, in spite of the fact that all solutions remained bounded in the phase space. This led to his famous question--“Does the flap of a butterfly’s wing in Brazil set off a tornado in Texas?”--that quickly become very well known, first and foremost among meteorologists and geophysicists, as “the butterfly effect.” The importance of the problem related to the Lorenz attractor inspired Smale to include it in his 18 important problems for the new millennium [2]. Tucker further studied the problem [3]. In the present paper, Immler presents a rigorous numerical algorithm by which Tucker’s computations can be formally verified. All these topics are thoroughly discussed in section 1.

The basic tools used in the verification process are ODE solvers and the Isabelle/HOL tool [4]. The ODE solvers are not presented in detail, but all needed information can easily be found in any of the numerous textbooks on this subject. Section 2 discusses Isabelle/HOL and dynamical systems.

Section 3 presents different concepts of “rigorous numerics,” which the paper defines as “computing with sets that are guaranteed to enclose real quantities of interest.” It also discusses Runge-Kutta methods for solving systems of ODEs together with remainders, as well as some topics related to affine arithmetic.

Section 4 is on computational geometry. The author verifies an algorithm presented by Girard and Le Guernic [5]. He also presents some details about an algorithm originally proposed by Donald Knuth.

Section 5 presents two different approaches for turning abstract formalizations into executable constructs: (1) lightweight data refinement, and (2) a dedicated framework for nondeterministic specifications and stepwise program refinement (the Autoref tool).

Computing Poincaré maps is presented in section 6. In connection with Tucker’s proof, both the Poincaré map and its derivative are needed (this is discussed in section 6.7). The algorithm needed for the formal verification of Tucker’s computations is called poincare.

All the tools (especially poincare) presented in sections 2 through 6 are applied in section 7 to formally verify the Lorenz attractor. Immler discusses “the input data and its interpretation” in section 7.1 and “checking the input data” in section 7.2.

The author’s major conclusion is summarized in section 8:

This article presented an overview of the diversity of algorithms, abstract results and techniques for the formal verification of a general-purpose ODE solver and its application to the rigorous numerical part of Tucker’s proof.

This section also includes remarks about future research (8.1), information about the size of the applied C++ code (8.2), additional information about Isabelle/HOL (8.3), and related works (8.4).

This well-written paper is important because it shows how the approximate methods of numerical analysis can be extended to prove rigorous theorems. It includes 49 references and is available under a Creative Commons license.