Explorable Proofs: Making Written Proofs Explorable by Grounding Them in Formal Representations
It is argued that grounding explanations in a formalized representation enables interactive affordances beyond what static text supports, and is instantiated for mathematical proof comprehension with explorable theorems, a system that uses LLMs to translate a theorem and its written proof into Lean, a programming langu...
Hita Kambhamettu, Will Crichton, S. Welleck et al.
· 0 citations