Explorable Theorems: Making Written Theorems Explorable by Grounding Them in Formal Representations
Authors: Hita Kambhamettu, Will Crichton, Sean Welleck, Harrison Goldstein, Andrew Head
Organizations: University of Pennsylvania Philadelphia, PA, USA · Brown University Providence, RI, USA · Carnegie Mellon University Pittsburgh, PA, USA · University at Buffalo Buffalo, SUNY, USA
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.
Figures & tables
Figure 1. Explorable theorems enlivens a static written proof with explorability affordances derived by analyzing and executing a linked formal machine proof. Given a written proof, a corresponding machine-checkable Lean proof is generated (\small1⃝). Structural and semantic information is derived by executing steps of the Lean proof (\small2⃝) and extracting logical dependencies (\small3⃝). This information is plugged into the written proof, allowing readers to use it as an explorable text. They can ask questions about whether a theorem holds on one or another example, the bounds of applicability, how the math “works out” for individual examples, and where counterexamples fail (\small4⃝). They can also ask questions about why propositions matter and where they come from by tracing to their definitions and uses (\small5⃝). Add your accessibility descriptions to the caption here.
Figure 2. The explorable theorems interface for the theorem “For all integers x , if x>2 , then x2−1 is not prime”. The input slider \small1⃝ lets readers set a concrete value of x ; color coding indicates where the theorem’s assumption x>2 holds. Each proof step is instantiated with Lean-verified intermediate values \small2⃝: for x=2 , the expression n=x2−1 evaluates to 3 . Clicking a variable such as n reveals the downstream proof steps that depend on it \small3⃝. When the concrete value violates the theorem’s assumptions, the interface flags exactly where the proof breaks \small4⃝, making the role of each assumption legible to the reader.
Figure 3. The pipeline for grounding interaction affordances in a formal representation. First, the Lean proof is generated (\small1⃝). The system executes this proof on concrete inputs and extract the Lean proof state (\small2⃝). A language model then generates a template for the proof step worked out on an example (\small4⃝). Lean-computed values are programmatically substituted into this template (\small6⃝) to produce the verified worked example shown to the reader. The consecutive states of the proof are diffed to create a dependency graph (\small3⃝). A mapping is created that links Lean statements to natural-language propositions (\small5⃝).
Figure 4. Instructor preferences by condition. Box plot shows the distribution of TrueSkill ratings assigned to participant responses through pairwise comparisons by a mathematics instructor, combined across both study tasks. The instructor preferred responses written with explorable theorems in 94.9% of pairwise comparisons.
Figure 5. Response quality by condition. Box plots show the distribution of graded correctness scores and percentage of responses referencing explicit proof steps, combined across both theorem tasks. Vertical lines within each box indicate the median. Responses written after using explorable theorems were graded as significantly more correct and referenced specific proof steps more frequently.
Figure 6. Timeline of proof-reading behavior for each participant during session. The y-axis indicates which proof step (1–8) the participant is engaging with. Blue circles and orange squares denote reading in the abstract and concrete (instantiation) views, respectively. Purple diamonds mark dependency link clicks.
Figure 7. Self-reported task load by condition. Box plots show the distribution of participant responses on a 1–7 agreement scale for four task load items, comparing explorable theorems to the baseline. Participants felt significantly less rushed and more successful with explorable theorems. No significant differences were found for mental demand or desire to use the tool in the future.