We present a dependent-type-based prover designed around the way LLMs (and humans) tend to write mathematics, complementing existing systems such as Lean and Rocq. Its core design choices are a surface that imitates mathematical natural language and a rule-driven automation layer that closes the routine steps a textbook would omit, so that an accepted proof can be re-emitted as a checked Lean file. Early experiments suggest that, even without any prover-specific training data, LLMs can learn to use it effectively on the miniF2F benchmark. Lean output excerpts: https://github.com/xiyuzhai-husky-lang/visored/

翻译：我们提出了一种基于依赖类型的证明器，其设计围绕大语言模型（以及人类）通常编写数学的方式展开，作为对现有系统如Lean和Rocq的补充。其核心设计选择包括：模仿数学自然语言的表层语法，以及通过规则驱动的自动化层来填补教科书通常会省略的常规步骤，从而使被接受的证明可重新输出为经过验证的Lean文件。初步实验表明，即使在没有任何针对证明器的训练数据的情况下，大语言模型也能在miniF2F基准测试中学会有效使用它。Lean输出示例见：https://github.com/xiyuzhai-husky-lang/visored/