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.

We present an incremental syntactic representation that consists of assigning a single discrete label to each word in a sentence, where the label is predicted using strictly incremental processing of a prefix of the sentence, and the sequence of labels for a sentence fully determines a parse tree. Our goal is to induce a syntactic representation that commits to syntactic choices only as they are incrementally revealed by the input, in contrast with standard representations that must make output choices such as attachments speculatively and later throw out conflicting analyses. Our learned representations achieve 93.72 F1 on the Penn Treebank with as few as 5 bits per word, and at 8 bits per word they achieve 94.97 F1, which is comparable with other state of the art parsing models when using the same pre-trained embeddings. We also provide an analysis of the representations learned by our system, investigating properties such as the interpretable syntactic features captured by the system and mechanisms for deferred resolution of syntactic ambiguities.