I am undertaking the task of formalizing Interval Newton Methods in Isabelle. To the best of my knowledge this hasn't been formalized in other proof assistants or theorem provers. However, I want to confirm this impression with you.
The methods I'm talking about are as described in Chapter 8 of Introduction to Interval Analysis. The idea would be to start verifying a one-dimensional version (reusing theories already present in Isabelle) and then extending it into a multivariate setting.
The most similar thing I have found come from ENS of Lyon where they have developed Gappa and produced this Phd thesis. But the first is a generic tool for floating points numbers and the second only deals with interval Newton methods collateraly.
Is there any reference you're aware of that provides a formalization of Interval Newton Methods in a proof assistant or theorem prover?
