将数学定理与可交互证明代码联动，让读者动手验证每一步推理。
Explorable Theorems: Making Written Theorems Explorable by Grounding Them in Formal Representations
- 用大模型把定理和证明转成可执行的Lean代码
- 用户可逐步调试、自测例子或反例，追踪逻辑依赖
- 实验证明互动式理解比纯阅读更准确深入
大模型生成的解释虽能提升技术内容可读性，但受限于静态文本无法交互。本文提出可探索定理系统，通过大模型将数学定理及其书面证明转化为可执行的Lean代码，并建立文本与代码的链接。读者可逐步推进证明、测试自定义例子或反例，并追溯每一步的逻辑依赖。每个步骤的结果由在具体例子上执行Lean证明并提取中间状态生成。用户研究（n=16）表明：在证明阅读任务中，使用可探索功能的参与者对理解问题的回答更准确、更完整，展现出更强的数学理解能力。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。