A Unifying Framework for Global Optimization: From Theory to Formalization

We introduce an abstract measure‑theoretic framework that serves as a tool to rigorously study stochastic iterative global optimization algorithms as a unified class. The framework is formulated in terms of probability kernels, which, via the Ionescu–Tulcea theorem, induce probability measures on the space of sequences of algorithm iterations, endowed with two intuitive properties. This framework answers the need for a general, implementation‑independent formalism in the analysis of such algorithms, providing a starting point for formalizing global optimization results in proof-assistants. To illustrate the relevance of our tool, we show that common algorithms fit naturally in the framework, and we also use it to give a rigorous proof of a general consistency theorem for stochastic iterative global optimization algorithms (Proposition 3 of (Malherbe, et al., 2017). This proof and the entire framework are formalized in the Lean proof assistant. This formalization both ensures the correctness of the definitions and proofs, and provides a basis for future machine-assisted formalizations in the field.