LeanSide combines natural language and proof verification for math learning
LeanSide: A Formally Verified Co-Reasoning System for Natural-language Proofs
Human-Computer Interaction
Summary
Writing accurate math proofs is hard because formal methods require very detailed steps, and AI tools can make mistakes. The authors developed LeanSide, a system that lets students write proofs in normal language while automatically checking them with a reliable, formal math assistant called Lean. It converts student ideas into formal proofs and explains feedback in simple terms. They tested LeanSide in classrooms to see what helped students understand proofs better and used those insights to improve the tool.
What this means in practice
- •For educational software developers: Integrate a user-friendly interface that translates student natural-language proofs into formal verification to enhance math learning tools.
- •For natural language processing engineers: Develop AI systems that co-operate with formal verifiers to provide reliable deductive reasoning support with understandable user feedback.
Authors
Chenjun Guo, Manooshree Patel, Arnav Mehta, Krishiv Kothari, Thomas Lu, Niels Voss, Rayna Bhattacharyya, Peter Donovan, Bjoern Hartmann, Gireeja Ranade
Abstract
Large language models are increasingly used as collaborators on deductive-reasoning tasks, but their outputs can hallucinate or pull users away from intended reasoning. Formal proof assistants provide machine-checked verification, but have a steep learning curve and require more granular reasoning than human written proofs. We explore an interface that combines these strengths, allowing users to write and revise free-form natural-language proofs while a verified backend checks their reasoning and returns feedback at the user's granularity. We study this interface in the context of undergraduate mathematics education by developing LeanSide, a formally verified co-reasoning system, which auto-formalizes student reasoning into Lean and informalizes verifier output into understandable feedback. We conducted user studies through classroom deployment and analyzed which system properties helped students make progress and which caused them to get stuck. We use these findings to derive design implications for using a formally verified backend in human-AI co-reasoning systems.