@inproceedings{zhang-etal-2026-autoformalization,
title = "Autoformalization {\&} Mathematical Reasoning",
author = "Zhang, Lan and
Valentino, Marco and
Meadows, Jordan and
Freitas, Andr{\'e}",
editor = "Marasovi{\'c}, Ana and
Glava{\v{s}}, Goran",
booktitle = "Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing: Tutorial Abstracts",
month = oct,
year = "2026",
address = "Budapest, Hungary",
publisher = "Association for Computational Linguistics",
url = "https://aclanthology.org/2026.emnlp-tutorials.4/",
pages = "6--7",
ISBN = "979-8-89176-463-7",
abstract = "Recent advances in large language models, formal reasoning, theorem proving, and agentic AI are rapidly changing what can be augmented and automated in mathematics. Yet mathematical reasoning is considerably richer than producing correct final answers: it involves understanding mathematical discourse, constructing and revising arguments, moving between informal and formal representations, exploring alternative proof strategies, verifying intermediate claims, and ultimately supporting mathematical discovery. This tutorial provides a structured introduction to the emerging field of automated mathematical reasoning, with a particular focus on autoformalization and neuro-symbolic and agentic approaches. We first examine mathematical reasoning from linguistic and conceptual perspectives, decomposing the spectrum from informal mathematical discourse to fully formal proofs. We then introduce the principal computational mechanisms underlying modern systems, including formal representations, autoformalization, theorem provers, critics and proxy evaluators, refinement loops, and complex agentic architectures. The tutorial connects these foundations with practical system-building, evaluation methodologies, current state-of-the-art results, and demonstrations of existing frameworks. We further examine how mathematical reasoning methods can extend toward physics, where mathematical arguments must interact with physical models, assumptions, approximations, and scientific knowledge. Finally, we use ambitious mathematical and scientific problems to identify the capabilities still required to move from benchmark solving toward systems that can participate meaningfully in verification, reasoning, and discovery."
}<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="zhang-etal-2026-autoformalization">
<titleInfo>
<title>Autoformalization & Mathematical Reasoning</title>
</titleInfo>
<name type="personal">
<namePart type="given">Lan</namePart>
<namePart type="family">Zhang</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Marco</namePart>
<namePart type="family">Valentino</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Jordan</namePart>
<namePart type="family">Meadows</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">André</namePart>
<namePart type="family">Freitas</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>Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing: Tutorial Abstracts</title>
</titleInfo>
<name type="personal">
<namePart type="given">Ana</namePart>
<namePart type="family">Marasović</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Goran</namePart>
<namePart type="family">Glavaš</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-463-7</identifier>
</relatedItem>
<abstract>Recent advances in large language models, formal reasoning, theorem proving, and agentic AI are rapidly changing what can be augmented and automated in mathematics. Yet mathematical reasoning is considerably richer than producing correct final answers: it involves understanding mathematical discourse, constructing and revising arguments, moving between informal and formal representations, exploring alternative proof strategies, verifying intermediate claims, and ultimately supporting mathematical discovery. This tutorial provides a structured introduction to the emerging field of automated mathematical reasoning, with a particular focus on autoformalization and neuro-symbolic and agentic approaches. We first examine mathematical reasoning from linguistic and conceptual perspectives, decomposing the spectrum from informal mathematical discourse to fully formal proofs. We then introduce the principal computational mechanisms underlying modern systems, including formal representations, autoformalization, theorem provers, critics and proxy evaluators, refinement loops, and complex agentic architectures. The tutorial connects these foundations with practical system-building, evaluation methodologies, current state-of-the-art results, and demonstrations of existing frameworks. We further examine how mathematical reasoning methods can extend toward physics, where mathematical arguments must interact with physical models, assumptions, approximations, and scientific knowledge. Finally, we use ambitious mathematical and scientific problems to identify the capabilities still required to move from benchmark solving toward systems that can participate meaningfully in verification, reasoning, and discovery.</abstract>
<identifier type="citekey">zhang-etal-2026-autoformalization</identifier>
<location>
<url>https://aclanthology.org/2026.emnlp-tutorials.4/</url>
</location>
<part>
<date>2026-10</date>
<extent unit="page">
<start>6</start>
<end>7</end>
</extent>
</part>
</mods>
</modsCollection>
%0 Conference Proceedings
%T Autoformalization & Mathematical Reasoning
%A Zhang, Lan
%A Valentino, Marco
%A Meadows, Jordan
%A Freitas, André
%Y Marasović, Ana
%Y Glavaš, Goran
%S Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing: Tutorial Abstracts
%D 2026
%8 October
%I Association for Computational Linguistics
%C Budapest, Hungary
%@ 979-8-89176-463-7
%F zhang-etal-2026-autoformalization
%X Recent advances in large language models, formal reasoning, theorem proving, and agentic AI are rapidly changing what can be augmented and automated in mathematics. Yet mathematical reasoning is considerably richer than producing correct final answers: it involves understanding mathematical discourse, constructing and revising arguments, moving between informal and formal representations, exploring alternative proof strategies, verifying intermediate claims, and ultimately supporting mathematical discovery. This tutorial provides a structured introduction to the emerging field of automated mathematical reasoning, with a particular focus on autoformalization and neuro-symbolic and agentic approaches. We first examine mathematical reasoning from linguistic and conceptual perspectives, decomposing the spectrum from informal mathematical discourse to fully formal proofs. We then introduce the principal computational mechanisms underlying modern systems, including formal representations, autoformalization, theorem provers, critics and proxy evaluators, refinement loops, and complex agentic architectures. The tutorial connects these foundations with practical system-building, evaluation methodologies, current state-of-the-art results, and demonstrations of existing frameworks. We further examine how mathematical reasoning methods can extend toward physics, where mathematical arguments must interact with physical models, assumptions, approximations, and scientific knowledge. Finally, we use ambitious mathematical and scientific problems to identify the capabilities still required to move from benchmark solving toward systems that can participate meaningfully in verification, reasoning, and discovery.
%U https://aclanthology.org/2026.emnlp-tutorials.4/
%P 6-7
Markdown (Informal)
[Autoformalization & Mathematical Reasoning](https://aclanthology.org/2026.emnlp-tutorials.4/) (Zhang et al., EMNLP 2026)
ACL
- Lan Zhang, Marco Valentino, Jordan Meadows, and André Freitas. 2026. Autoformalization & Mathematical Reasoning. In Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing: Tutorial Abstracts, pages 6–7, Budapest, Hungary. Association for Computational Linguistics.