Visored：一种用于 LLM 生成数学证明的控制自然语言证明器

本文提出了一种基于依赖类型的证明器 Visored，其设计契合大语言模型（及人类）书写数学的习惯，是对 Lean 和 Rocq 等现有系统的补充。其核心设计包括模仿数学自然语言的表面层，以及能自动补全教科书省略的常规步骤的规则驱动自动化层，使被接受的证明可重新输出为经检查的 Lean 文件。初步实验表明，即使未经特定训练，LLM 也能在 miniF2F 基准上有效使用该工具进行数学推理。