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.

翻译：大语言模型生成的解释能使技术内容更易理解，但其交互能力存在固有局限。由于LLM输出为静态文本，无法执行或逐步浏览。我们提出，将解释锚定在形式化表征中，能够实现超越静态文本的交互功能。我们通过“可探索定理”系统将该理念应用于数学证明理解：该系统利用LLM将定理及其书面证明转化为Lean（一种面向机器验证证明的编程语言），并将书面证明与Lean代码建立关联。读者可逐步骤细粒度浏览证明过程，测试定制示例或反例，并追溯连接各步骤的逻辑依赖关系。每个展开步骤均通过执行针对该示例的Lean证明并提取其中间状态生成。一项用户研究（n=16）表明该方法具有潜在优势：在证明校对任务中，能够使用所提供的可探索功能的参与者，给出了更优、更准确且更详细的阅读理解答案，展现出对底层数学概念更全面的理解。