机器辅助定理证明是指通过结构化推理自动生成数学定理证明的过程。最近，人们对结合使用机器学习模型和证明助手来执行这项任务的兴趣激增。本文介绍了Pantograph，这是一个为Lean 4证明助手提供通用接口的工具，它可以通过强大的搜索算法（如蒙特卡洛树搜索）实现高效的证明搜索。此外，Pantograph通过更稳健地处理Lean 4的推理步骤，实现了更高层次的推理。本文概述了Pantograph的架构和功能。我们还报告了一个说明性用例：使用机器学习模型和证明草图来证明Lean 4定理。Pantograph的创新功能为更先进的机器学习模型执行复杂的证明搜索和高层次推理铺平了道路，使未来的研究人员能够设计出更通用和强大的定理证明器。