A Lean 4 Framework for the Radii Polynomial Method
Fengyang Wang
math.DS
Oct 1, 2026 · v1
TL;DR
Formalizes the radii polynomial method for computer-assisted proofs in Lean 4 with Mathlib, checking rational certificates for Taylor/Chebyshev series examples including Lorenz.
Abstract
Computer-assisted proofs in dynamics establish results about nonlinear systems by rigorous numerical computation. Their correctness rests on a trusted base of interval-arithmetic libraries and analytic estimates checked by hand. We formalize in Lean 4 a framework for the radii polynomial method, which certifies an exact solution near a numerical approximation by verifying four norm bounds and the resulting polynomial inequality. Weighted coefficient algebras provide the common setting for polynomial equations and initial value problems in Taylor and Chebyshev series. Their universal properties construct the bounded operators and the evaluation maps, and the universal property of the free commutative algebra makes polynomial substitution commute with evaluation. Finite/tail reductions turn the four norm bounds into finite rational inequalities, which are checked in Lean. The radii theorem then yields an exact coefficient solution, and realization theorems carry it to a solution of the original equation. The worked examples are a square-root branch given by a convergent power series and polynomial initial value problems, among them the Lorenz system, for which the library proves existence, uniqueness within the trajectory ball, and analyticity of the function-level solution.
Problem
Computer-assisted proofs in dynamics depend on trusted interval-arithmetic libraries and on analytic estimates checked by hand. The radii polynomial method, which certifies an exact solution near a numerical approximation, had no machine-checked foundation.
Approach
The radii polynomial theorem for Banach-space maps is proved in Lean 4 using Mathlib's mean value and contraction mapping theorems. Weighted ℓ¹ coefficient algebras over index monoids are built with universal properties that yield bounded operators, evaluation maps, and commutation of polynomial substitution with evaluation. Finite/tail decompositions reduce the four norm bounds to finite rational inequalities, which are checked in Lean, partly via LeanCert tactics. Realization theorems then turn exact coefficient solutions into solutions of the original equations.
Results
End-to-end certified examples cover a square-root branch given by a power series and polynomial initial value problems in Taylor and Chebyshev series. For the Lorenz system, the library proves existence, uniqueness within the trajectory ball, and analyticity of the function-level solution. Some infrastructure, including a discrete-convolution API, was contributed to Mathlib.
