# Explorable Proofs: Making Written Proofs Explorable by Grounding Them in Formal Representations

arXiv: https://arxiv.org/abs/2604.02598 · HTML: https://mlsanity.com/paper/2604.02598/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 4 of its 79 references that are in the map.
- First posted on arXiv 3 Apr 2026.

## Builds on (most cited first, 4 of 4)

- [LeanReasoner: Boosting Complex Logical Reasoning with Lean](https://mlsanity.com/paper/2403.13312/) (2024)
- [DataTales: Investigating the use of Large Language Models for Authoring Data-Driven Articles](https://mlsanity.com/paper/2308.04076/) (2023)
- [VeriPlan: Integrating Formal Verification and LLMs into End-User Planning](https://mlsanity.com/paper/2502.17898/) (2025)
- [Augmented Physics: Creating Interactive and Embedded Physics Simulations from Static Textbook Diagrams](https://mlsanity.com/paper/2405.18614/) (2024)

## Abstract (arXiv)

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.