@inproceedings{mehta-etal-2026-formally,
title = "Formally Verified {AI} Co-Reasoning: An Education Case Study",
author = "Mehta, Arnav and
Guo, Chenjun and
Lu, Thomas and
Voss, Niels and
Patel, Manooshree and
Bhattacharyya, Rayna and
Donovan, Peter and
Ranade, Gireeja",
editor = "Lee, Hung-Yi and
Dev, Sunipa and
Li, Jessy and
Elliott, Desmond",
booktitle = "Findings of the {A}ssociation for {C}omputational {L}inguistics: {EMNLP} 2026",
month = oct,
year = "2026",
address = "Budapest, Hungary",
publisher = "Association for Computational Linguistics",
url = "https://aclanthology.org/2026.findings-emnlp.977/",
pages = "20651--20668",
ISBN = "979-8-89176-462-0",
abstract = "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.\par 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."
}<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="mehta-etal-2026-formally">
<titleInfo>
<title>Formally Verified AI Co-Reasoning: An Education Case Study</title>
</titleInfo>
<name type="personal">
<namePart type="given">Arnav</namePart>
<namePart type="family">Mehta</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Chenjun</namePart>
<namePart type="family">Guo</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Thomas</namePart>
<namePart type="family">Lu</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Niels</namePart>
<namePart type="family">Voss</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Manooshree</namePart>
<namePart type="family">Patel</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Rayna</namePart>
<namePart type="family">Bhattacharyya</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Peter</namePart>
<namePart type="family">Donovan</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Gireeja</namePart>
<namePart type="family">Ranade</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<originInfo>
<dateIssued>2026-10</dateIssued>
</originInfo>
<typeOfResource>text</typeOfResource>
<relatedItem type="host">
<titleInfo>
<title>Findings of the Association for Computational Linguistics: EMNLP 2026</title>
</titleInfo>
<name type="personal">
<namePart type="given">Hung-Yi</namePart>
<namePart type="family">Lee</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Sunipa</namePart>
<namePart type="family">Dev</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Jessy</namePart>
<namePart type="family">Li</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Desmond</namePart>
<namePart type="family">Elliott</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<originInfo>
<publisher>Association for Computational Linguistics</publisher>
<place>
<placeTerm type="text">Budapest, Hungary</placeTerm>
</place>
</originInfo>
<genre authority="marcgt">conference publication</genre>
<identifier type="isbn">979-8-89176-462-0</identifier>
</relatedItem>
<abstract>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.\par 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.</abstract>
<identifier type="citekey">mehta-etal-2026-formally</identifier>
<location>
<url>https://aclanthology.org/2026.findings-emnlp.977/</url>
</location>
<part>
<date>2026-10</date>
<extent unit="page">
<start>20651</start>
<end>20668</end>
</extent>
</part>
</mods>
</modsCollection>
%0 Conference Proceedings
%T Formally Verified AI Co-Reasoning: An Education Case Study
%A Mehta, Arnav
%A Guo, Chenjun
%A Lu, Thomas
%A Voss, Niels
%A Patel, Manooshree
%A Bhattacharyya, Rayna
%A Donovan, Peter
%A Ranade, Gireeja
%Y Lee, Hung-Yi
%Y Dev, Sunipa
%Y Li, Jessy
%Y Elliott, Desmond
%S Findings of the Association for Computational Linguistics: EMNLP 2026
%D 2026
%8 October
%I Association for Computational Linguistics
%C Budapest, Hungary
%@ 979-8-89176-462-0
%F mehta-etal-2026-formally
%X 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.\par 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.
%U https://aclanthology.org/2026.findings-emnlp.977/
%P 20651-20668
Markdown (Informal)
[Formally Verified AI Co-Reasoning: An Education Case Study](https://aclanthology.org/2026.findings-emnlp.977/) (Mehta et al., Findings 2026)
ACL
- Arnav Mehta, Chenjun Guo, Thomas Lu, Niels Voss, Manooshree Patel, Rayna Bhattacharyya, Peter Donovan, and Gireeja Ranade. 2026. Formally Verified AI Co-Reasoning: An Education Case Study. In Findings of the Association for Computational Linguistics: EMNLP 2026, pages 20651–20668, Budapest, Hungary. Association for Computational Linguistics.