Explorable Theorems: Making Written Theorems Explorable by Grounding Them in Formal Representations
Hita Kambhamettu, Will Crichton, Sean Welleck, Harrison Goldstein, Andrew Head
cs.HC
Apr 3, 2026 · v1
TL;DR
Uses LLMs to translate a written theorem and proof into Lean, then executes the Lean proof on examples to extract intermediate states for interactive exploration.
Abstract
LLM-generated explanations can make technical content more accessible, but there is a ceiling on what they can support interactively. Because LLM outputs are static text, they cannot be executed or stepped through. We argue that grounding explanations in a formalized representation enables interactive affordances beyond what static text supports. We instantiate this idea for mathematical proof comprehension with explorable theorems, a system that uses LLMs to translate a theorem and its written proof into Lean, a programming language for machine-checked proofs, and links the written proof with the Lean code. Readers can work through the proof at a step-level granularity, test custom examples or counterexamples, and trace the logical dependencies bridging each step. Each worked-out step is produced by executing the Lean proof on that example and extracting its intermediate state. A user study ($n = 16$) shows potential advantages of this approach: in a proof-reading task, participants who had access to the provided explorability features gave better, more correct, and more detailed answers to comprehension questions, demonstrating a stronger overall understanding of the underlying mathematics.
Problem
LLM-generated explanations of mathematical proofs are static text that cannot be executed or stepped through, limiting interactive comprehension. Readers cannot test examples, trace dependencies, or explore proofs at fine granularity.
Approach
Explorable Theorems is a system that uses LLMs to translate a theorem and its written proof into Lean, then links the written proof with the Lean code. Readers can work through the proof at step-level granularity, test custom examples or counterexamples, and trace logical dependencies bridging each step. Each worked-out step is produced by executing the Lean proof on that example and extracting its intermediate state.
Results
A user study (n=16) shows that participants with access to explorability features gave better, more correct, and more detailed answers to comprehension questions in a proof-reading task, demonstrating stronger overall understanding of the underlying mathematics compared to a control group.
