This tutorial introduces autoformalization using Large Language Models (LLMs), covering theorem provers, retrieval-augmented generation, refinement with formal feedback, evaluation techniques, and applications to scientific discovery.
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.
The tutorial slides are accessible here.
The demonstration is accessible here.
The full recording is accessible here.
Understand autoformalization: how informal mathematical statements in natural language/LaTeX are translated into formal languages that theorem provers can verify.
Learn the basics of formal systems, especially Isabelle and Lean4, including examples from existing formal mathematical libraries.
Explore LLM-based autoformalization, including zero-shot, few-shot, and retrieval-augmented approaches, and understand their main limitations.
Learn refinement techniques using feedback, including theorem-prover error messages for syntactic correction and LLM-based feedback for semantic refinement
Understand how autoformalizations are evaluated, including reference-based metrics and emerging LLM-as-a-Judge/reference-free methods.
See applications beyond pure mathematics, particularly human-in-the-loop autoformalization for physics and scientific discovery.
Lower the barrier to entry for NLP researchers and encourage interdisciplinary work connecting NLP, theorem proving, formal reasoning, and AI for science.
Time Topic
10 min Motivation
10 min Understanding Mathematical Discourse
10 min Defining Mathematical Reasoning
10 min Neuro-symbolic Methods
10 min Q&A
30 min Building Mathematical Reasoning Systems + Q&A
30 min Evaluation
30 min Methods and State of the Art + Q&A
30 min Real-World Applications & Broader Implications
10 min Concluding Remarks
Wednesday, October 28, Budapest, Hungary
EMNLP 2026
Lan is a PhD student in the Department of Computer Science in University of Manchester. His research interest mainly focuses on autoformalization and formal mathematical reasoning. He has published papers at major NLP conferences, including ACL, EMNLP, and NAACL. His contributions to autoformalization were recognized with the Best Resource Paper Award at EMNLP 2025, highlighting the impact of his work on formal mathematical reasoning and verification.
Marco is a Lecturer in Artificial Intelligence and Applications of AI in the Natural Language Processing (NLP) group at the University of Sheffield. Prior to Sheffield, he was a member of the Neuro-Symbolic AI Group at the Idiap Research Institute in Switzerland, and obtained a PhD in Computer Science from the University of Manchester. His research focuses on developing AI systems that can use explanation as a core mechanism for learning and reasoning, investigating the integration of neural and symbolic AI methods. Moreover, he is interested in developing methodologies to interpret, control, and evaluate Large Language Models (LLMs), with a focus on disentangling knowledge acquisition from abstract logical reasoning, and enabling out-of-distribution, out-of-domain generalisation. His research on neuro-symbolic NLP received a best resource paper award at EMNLP 2025 and an outstanding paper award at EMNLP 2024.
Jordan Meadows is a Postdoctoral Researcher at Idiap Research Institute working on natural language processing, neuro-symbolic AI, and AI for Science. He received his PhD in Computer Science from the University of Manchester, where he studied mathematical language processing and the reasoning capabilities of language models. His research focuses broadly on mathematical and scientific reasoning, with particular interest in combining language models with symbolic methods to make AI systems more reliable, interpretable, and verifiable. His work has been published across major NLP and AI venues, and he has presented research on mathematical reasoning and the autoformalisation of science to both academic and interdisciplinary audiences.
André Freitas leads the Neuro-symbolic AI Lab at the University of Manchester and IDIAP Research Institute. His main research interests are on enabling the development of AI methods to support abstract, flexible and controlled reasoning in order to support AI-augmented scientific discovery. In particular, he investigates how the combination of neural and symbolic data representation paradigms can deliver better models of inference. He is an active contributor to the main conferences and journals in the AI/Natural Language Processing (NLP) interface (AAAI, NeurIPS, ACL, EMNLP, EACL, COLING, TACL, Computational Linguistics), with over 100 peer-reviewed publications.
The following papers provide useful background for the topics covered in the tutorial.
Wu et al. (2022), Autoformalization with Large Language Models
Zhang et al. (2024), Consistent Autoformalization for Constructing Mathematical Libraries
Liu et al. (2025), Rethinking and Improving Autoformalization: Towards a Faithful Metric and a Dependency Retrieval-Based Approach
Wang et al. (2026), Aria: An Agent for Retrieval and Iterative Auto-Formalization via Dependency Graph
Lu et al. (2024), Process-Driven Autoformalization in Lean 4
Zhang et al. (2025), Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions
Zhang et al. (2025), MASA: LLM-Driven Multi-Agent Systems for Autoformalization
Zhang et al. (2026), Monotonic Reference-Free Refinement for Autoformalization
Li et al. (2024), Autoformalizing Mathematical Statements by Symbolic Equivalence and Semantic Consistency
Zhang et al. (2025), Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning
Poiroux et al. (2025), Reliable Evaluation and Benchmarks for Statement Autoformalization
Lu et al. (2025), FormalAlign: Automated Alignment Evaluation for Autoformalization
Xuejun et al. (2026), Mathesis: Towards Formal Theorem Proving from Natural Languages
Jiang et al. (2024), Multi-Language Diversity Benefits Autoformalization
Ying et al. (2024), Lean Workbook: A Large-Scale Lean Problem Set Formalized from Natural Language Math Problems
Gao et al. (2025), Herald: A Natural Language Annotated Lean 4 Dataset
Peng et al. (2025), CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization
Liu et al. (2025), ATLAS: Autoformalizing Theorems Through Lifting, Augmentation, and Synthesis of Data