Although there are several systems that successfully generate construction steps for ruler and compass construction problems, none of them provides readable synthetic correctness proofs for generated constructions. In the present work, we demonstrate how our triangle construction solver ArgoTriCS can cooperate with automated theorem provers for first order logic and coherent logic so that it generates construction correctness proofs, that are both human-readable and formal (can be checked by interactive theorem provers such as Coq or Isabelle/HOL). These proofs currently rely on many high-level lemmas and our goal is to have them all formally shown from the basic axioms of geometry.

翻译：尽管已有多个系统能够成功生成尺规作图问题的构造步骤，但其中没有任何一个能为生成的构造提供可读的合成正确性证明。在本文中，我们展示了三角形构造求解器ArgoTriCS如何与一阶逻辑和相干逻辑的自动定理证明器协作，从而生成既具有人类可读性又具备形式化特征（可通过Coq或Isabelle/HOL等交互式定理证明器检查）的构造正确性证明。目前这些证明依赖于大量高层引理，我们的目标是基于几何基本公理对所有引理进行形式化证明。