2 citations · 3 across the 4 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2024
Towards Automatic Transformations of Coq Proof Scripts
Nicolas Magaud
Proof assistants like Coq are increasingly popular to help mathematicians carry out proofs of the results they conjecture. However, formal proofs remain highly technical and are es…
cs.LO2022
Spreads and Packings of PG(3,2), Formally!
Nicolas Magaud
We study how to formalize in the Coq proof assistant the smallest projective space PG(3,2). We then describe formally the spreads and packings of PG(3,2), as well as some of their…
cs.LO2021★ 1 cited
Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant
Nicolas Magaud
Recently, we developed an automated theorem prover for projective incidence geometry. This prover, based on a combinatorial approach using matroids, proceeds by saturation using th…