@tao The research group around Sylvie Boldo has done a great deal of work on verified computer arithmetic in Rocq, in case you ever have to go beyond 17th century methods. For example, they formalized numerical methods for Lebesgue intergration. Here are some relevant links for reference: https://pages.saclay.inria.fr/sylvie.boldo/research.html, https://depot.lipn.univ-paris13.fr/mayero/rocq-num-analysis P.S. I should also mention Assia Mahboubi and https://fresco.gitlabpages.inria.fr – their work is quite relevant here as well.