Yes, whose history if I’m not mistaken starts with this paper and then continues on over a couple others

The CAD has been implemented in Coq indeed by Assia Mahboubi. However the formal proof was never completed. Mathcomp did not exist at the time. Many years later with Boris Djalal, we tried to reprogram and prove it using https://github.com/math-comp/real-closed and https://github.com/math-comp/cad. But this was never finished.

Got it, thank you

Luigi Massacci has marked this topic as resolved.

Last updated: Jun 23 2024 at 04:03 UTC