Quokka

语料库级形式化数学：ReasBook 文档、持续增长的 formal corpus，以及从文献解析到 Lean 验证的工具链。

演示视频

核心能力

• ReasBook 输出保留章节结构、定义、定理与证明（如《Analysis II》）。
• 语料库级流水线覆盖 Stacks Project、教材、讲义与论文。
• 单证明形式化：自然语言 → Lean 陈述 → 在 ReasLab 中验证完整证明。
• 补全含 sorry 的 Lean 代码；解析 PDF、TeX、Markdown 或图片为结构化 JSON。
• 在 ReasLab 中对 AI 生成的形式化代码进行人工审阅与评论。

开始使用

• Lean 形式化指南 · Lean 工具链