本文介绍了交互式定理证明器（又称证明助手），这种工具可以创建严格的、机器可检查的数学定理和计算证明。文章以 Lean 为例，展示了如何使用证明助手来验证数学证明的正确性，并探讨了证明助手在零知识虚拟机（zkVM）开发中的应用。
zksecurity