Research Paper Formalization
From a research manuscript to an independently inspectable Lean development: perform the formalization workflow with Quokka, verify the formal proof in ReasLab, and use the theorem dependency graph to understand how theorems depend on one another.
Demo Video
Highlights
- Read the theorem in its original manuscript context and locate the corresponding formal statement.
- Use Quokka to carry out the related formalization workflow and produce the Lean development.
- Inspect and verify the formal proof in ReasLab with live compiler feedback and Infoview results.
- Follow imported definitions and intermediate lemmas through editor navigation.
- Confirm that the formal proof closes under Lean's kernel checks.
- Use the theorem dependency graph to gain a deeper understanding of the relationships among theorems.