Conjecturing and theorem proving are activities at the center of mathematical practice and are difficult to separate. In this paper, we propose a framework for completing incomplete conjectures and incomplete proofs. The framework can turn a conjecture with missing assumptions and with an under-specified goal into a proper theorem. Also, the proposed framework can help in completing a proof sketch into a human-readable and machine-checkable proof. Our approach is focused on synthetic geometry, and uses coherent logic and constraint solving. The proposed approach is uniform for all three kinds of tasks, flexible and, to our knowledge, unique such approach.

翻译：猜想与定理证明是数学实践的核心活动，且两者难以分离。本文提出一个用于补全不完整猜想与不完整证明的框架。该框架能将缺少假设且目标未完全定义的猜想转化为恰当定理，同时也能帮助将证明草图补全为人类可读且机器可验证的证明。我们的方法聚焦于合成几何，采用相干逻辑与约束求解技术。所提出的方法对三类任务具有统一性、灵活性，据我们所知，也是唯一具有此类特性的方法。