Formally Verified AI Co-Reasoning: An Education Case Study

Proof assistants such as Lean4 offer machine-checkable verification of mathematical reasoning, but their adoption is limited because formal languages have a steep learning curve and can be challenging to use. Large language models offer a way to lower this barrier to entry through natural-language co-reasoning systems: proof assistants that users interact with entirely in natural language, and which use formal verification to provide feedback to users who submit incomplete and incorrect proofs. This paper explores such a co-reasoning system in an educational setting. At the core of such systems is an auto-formalizer that must faithfully translate natural-language arguments into formal proofs. This faithful auto-formalization, for an educational setting, is the focus of this work. We make three contributions. First, we identify desiderata for natural language co-reasoning systems--faithfulness, accuracy, appropriate granularity, transparency, and incremental editability. Second, we introduce an evaluation framework for the first three of these properties in the context of educational proofs. Third, we present a case study on an educational natural-language co-reasoning system for math proofs, whose auto-formalization harness we evaluate on student-written proofs from an undergraduate linear algebra class against the three desiderata.