Explorable Theorems: Making Written Theorems Explorable by Grounding Them in Formal Representations
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866915930150273024 |
|---|---|
| author | Kambhamettu, Hita Crichton, Will Welleck, Sean Goldstein, Harrison Head, Andrew |
| author_facet | Kambhamettu, Hita Crichton, Will Welleck, Sean Goldstein, Harrison Head, Andrew |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_02598 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Explorable Theorems: Making Written Theorems Explorable by Grounding Them in Formal Representations Kambhamettu, Hita Crichton, Will Welleck, Sean Goldstein, Harrison Head, Andrew Human-Computer Interaction Artificial Intelligence Programming Languages 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. |
| title | Explorable Theorems: Making Written Theorems Explorable by Grounding Them in Formal Representations |
| topic | Human-Computer Interaction Artificial Intelligence Programming Languages |
| url | https://arxiv.org/abs/2604.02598 |