Proof assistants such as Lean 4 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.

We explore metrics for three properties that are important for natural language co-reasoning systems—faithfulness, accuracy and appropriate granularity. We introduce an evaluation framework for these properties in the context of educational proofs. Second, we present a case study on an educational natural-language co-reasoning system for math proofs, evaluating its autoformalization harness on student-written proofs from an undergraduate linear algebra class using these three properties.