哪些自动定理证明器能够输出自然语言形式的证明？

大多数基于归结法的自动定理证明器生成的证明因依赖机器内部逻辑，难以被人类直接理解。以下是一些能输出自然语言或类人风格可读证明的工具及相关研究成果：

• Isabelle/Isar：交互式定理证明器，支持以结构化、类数学论文风格的Isar语言编写证明，生成的证明文本接近人类撰写的数学论证，可读性强。同时支持自动战术（如auto、simp）辅助生成证明框架，可直接输出或经少量调整得到可读证明。
• Coq + Coqdoc：Coq的证明脚本可通过Coqdoc转换为LaTeX或HTML格式的结构化文档，配合Proof using等规范写法，能生成清晰的证明过程。部分扩展插件可将Coq证明进一步转换为自然语言文本。
• Lean Theorem Prover：其证明语言设计注重可读性，官方维护的mathlib库中大量证明采用接近自然数学语言的风格书写。Lean支持将证明导出为结构化文本，部分工具可转换为自然语言描述。
• Automath：早期自动化定理证明系统，以结构化的自然语言风格表示证明，是类人可读证明领域的先驱工作，对后续研究有重要启发。
• NatDed：专注于自然演绎风格的证明生成，输出的证明遵循人类常用的自然推理步骤，格式清晰易懂，适合教学和基础逻辑证明场景。

你提到的由M. Ganesalingam和W. T. Gowers开发的具备类人风格输出的全自动问题求解器是该领域的重要成果，它针对数学竞赛类问题生成接近人类数学家风格的自然语言证明，在自动生成类人证明的自动化程度上有突破性进展。

内容的提问来源于stack exchange，提问作者Julien Narboux