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: Oct 13 2024 at 01:02 UTC