{"id":"arxiv/2610.02335","url":"https://arxiv.org/abs/2610.02335","tags":["math.DS"],"score":0,"title":"A Lean~4 Framework for the Radii Polynomial Method","domain":"math.DS","source":"arxiv","authors":["Fengyang Wang"],"reviews":0,"subject":"math.DS","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-10-01","reactions":{}}