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.

翻译：通过大语言模型生成的解释可以提升技术内容的可理解性，但其交互支持存在天花板。由于大语言模型输出的是静态文本，无法执行或逐步推进。我们认为，将解释锚定在形式化表示中能够实现超越静态文本的交互能力。我们通过"可探索定理"系统将这一理念付诸实践，该系统利用大语言模型将定理及其书面证明翻译成Lean（一种用于机器验证证明的编程语言），并将书面证明与Lean代码建立关联。读者可以按步骤粒度研读证明，测试自定义示例或反例，并追溯连接各步骤的逻辑依赖关系。每个展开步骤均通过执行该示例的Lean证明并提取其中间状态生成。一项用户研究（n=16）表明该方法具有潜在优势：在校对任务中，获得可探索功能的参与者对理解问题的回答更准确、更详尽，展现出对底层数学概念更全面的整体理解。