For a wide range of values of the incoming solar radiation, the Earth features at least two attracting states, which correspond to competing climates. The warm climate is analogous to the present one, the snowball climate features global glaciation and conditions that can hardly support life forms. Paleoclimatic evidences suggest that in past our planet flipped between these two states. The main physical mechanism responsible for such instability is the ice-albedo feedback. In a previous work, we defined the Melancholia states that sit between the two climates. Such states are embedded in the boundaries between the two basins of attraction and feature extensive glaciation down to relatively low latitudes. Here, we explore the global stability properties of the system by introducing random perturbations as modulations to the intensity of the incoming solar radiation. We observe noise-induced transitions between the competing basins of attractions. In the weak noise limit, large deviation laws define the invariant measure and the statistics of escape times. By empirically constructing the instantons, we show that the Melancholia states are the gateways for the noise-induced transitions. In the region of multistability, in the zero-noise limit, the measure is supported only on one of the competing attractors. For low (high) values of the solar irradiance, the limit measure is the snowball (warm) climate. The changeover between the two regimes corresponds to a first order phase transition in the system. The framework we propose seems of general relevance for the study of complex multistable systems. At this regard, we relate our results to the debate around the prominence of contigency vs. convergence in biological evolution. Finally, we propose a new method for constructing Melancholia states from direct numerical simulations, thus bypassing the need to use the edge-tracking algorithm.[-]

This talk is about verified numerical algorithms in Isabelle/HOL, with a focus on guaranteed enclosures for solutions of ODEs. The enclosures are represented by zonotopes, arising from the use of affine arithmetic. Enclosures for solutions of ODEs are computed by set-based variants of the well-known Runge-Kutta methods.
All of the algorithms are formally verified with respect to a formalization of ODEs in Isabelle/HOL: The correctness proofs are carried out for abstract algorithms, which are specified in terms of real numbers and sets. These abstract algorithms are automatically refined towards executable specifications based on lists, zonotopes, and software floating point numbers. Optimizations for low-dimensional, nonlinear dynamics allow for an application highlight: the computation of an accurate enclosure for the Lorenz attractor. This contributes to an important proof that originally relied on non-verified numerical computations.[-]