Naproche 发布：用受控自然语言写数学证明的助手

开发者 zetalyrae 分享了证明助手项目 Naproche，其输入语言是嵌入 LaTeX 的受控自然语言，风格类似 Inform7，贴近数学家的叙述习惯。它并非单纯的证明检查器，而是将自然语言数学证明翻译为公式表示，并为每个证明步骤生成证明义务加以验证，让形式化证明更易被数学家读写。

2026-09-23 ~ 2026-09-23 · 2 条相关

• Naproche:用受控自然语言写数学证明的证明助手 — zetalyrae · 2026-09-23

另有 1 条近重复转述:zetalyrae