Dependently-typed proof assistants furnish expressive foundations for mechanised mathematics and verified software. However, automation for these systems has been either modest in scope or complex in implementation. We aim to improve the situation by integrating proof assistants with automated theorem provers (ATPs) in a simple way, while preserving the correctness guarantees of the former. A central difficulty arises from the fact that most ATPs operate in classical first-order logic, whereas these proof assistants are grounded in constructive dependent type theory. We identify an expressive fragment of both languages -- essentially equational Horn -- that admits sound, straightforward translations in both directions. The approach produces a prototype system for Agda forwarding proof obligations to the ATP Vampire, then transforming the resulting classical proof into a constructive proof term that Agda can type-check. The prototype automatically derives proofs concerning the properties of a complex field equipped with roots of unity, which took professional Agda developers two full days to complete. The required engineering effort is modest, and we anticipate that the methodology will extend readily to other ATPs and proof assistants.

翻译：依赖类型证明助手为机械化数学与可验证软件提供了富有表达力的基础。然而，这些系统的自动化程度要么范围有限，要么实现复杂。我们旨在通过以简洁的方式将证明助手与自动定理证明器（ATP）集成，同时保持前者的正确性保证，以改善这一现状。一个核心难点在于，大多数ATP基于经典一阶逻辑运行，而这些证明助手则建立在构造性依赖类型理论之上。我们识别出两种语言中一个富有表达力的片段——本质上是等式Horn子句——该片段允许在两个方向上实现可靠且直接的转换。该方法构建了一个原型系统，可将Agda中的证明义务转发给ATP Vampire，随后将得到的经典证明转化为Agda能够类型检查的构造性证明项。该原型系统能自动推导关于配备单位根的复数域性质的证明，而同样的证明曾需要专业的Agda开发者耗费整整两天时间完成。所需的工程实现成本较低，我们预期该方法能轻松扩展至其他ATP与证明助手。