Explorable Theorems: Making Written Theorems Explorable by Grounding Them in Formal Representations

TL;DR

This paper introduces explorable theorems, a system that grounds mathematical explanations in formal Lean code, enabling interactive proof exploration and improving comprehension.

Contribution

It presents a novel system that translates written theorems into Lean, linking explanations with formal proofs for interactive exploration.

Findings

Participants with explorable features answered comprehension questions more accurately.

The system allows step-by-step proof execution and testing of examples.

Explorable theorems enhance understanding of mathematical proofs.

Abstract

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.