The method of radii polynomials provides rigorous proofs for solutions of ODEs and PDEs by combining numerical solutions with interval arithmetic and the Banach fixed-point theorem. We present an ongoing project towards a general Lean framework for formally verifying these proofs. Joint work with Heather Macbeth and Mario Carneiro.