Quokka
Corpus-scale formal mathematics: ReasBook documents, growing formal corpora, and tooling from literature parsing to verified Lean proofs.
Demo Video
Highlights
- ReasBook output with chapter structure, definitions, theorems, and proofs (e.g., Analysis II).
- Corpus-level pipeline across Stacks Project, textbooks, lecture notes, and papers.
- Single-proof formalization: natural language → Lean statement → full proof in ReasLab.
- Lean proof completion for code with
sorry; literature parsing from PDF, TeX, Markdown, or images. - Human review and comments on AI-generated formal code in ReasLab.