Math foundation formalization agent unifies proof creation and verification
Math Foundation Formalization Agent: A General-Purpose Approach to Formalizing Mathematical Foundations
Logic in Computer ScienceArtificial Intelligence
Summary
Making sure math proofs are perfectly correct and understandable by computers is very important but hard to do manually. The authors created an intelligent agent that combines smart language models with a proof-checking system to help write and check math proofs across many math areas. This tool works on different math foundations like set theory and logic by generating, refining, and verifying formal proofs automatically. Their tests show it is possible to have one system handle many foundational math tasks, highlighting both its potential and current limitations.
What this means in practice
- •For formal methods engineers: Auto-generate and verify foundational mathematical proofs to support development of formally verified software and hardware.
- •For mathematical knowledge engineers: Use a unified agent to assist in building, refining, and managing formal mathematical libraries across multiple foundational domains.
Authors
Jiaxin Xie, Guowei Dou, Xiang Ji, Wensheng Yu
Abstract
Mathematical formalization plays an important role in establishing rigorous and machine-verifiable foundations for mathematical reasoning. With the development of large language models (LLMs) and interactive theorem provers, intelligent agents offer a promising approach to automating the formalization of mathematical theories. This paper presents the Math Foundation Formalization Agent (MFF-Agent), a general-purpose intelligent agent designed to support formalization tasks across multiple mathematical domains. The agent integrates the reasoning capabilities of large language models with the formal verification capabilities of the Rocq proof assistant. It incorporates task classification, tool-assisted execution, verification feedback, and state-based task management to support the generation, refinement, and verification of formal proofs. Unlike an approach focused on a single mathematical theory, the agent is examined through case studies involving Morse--Kelley axiomatic set theory (MK), real numbers, propositional logic, and equivalences of the axiom of choice. These cases investigate its applicability across mathematical foundations and distinguish source-level completion, interactive verification, and reproducible compilation. The results demonstrate the feasibility of a unified operational framework for heterogeneous foundation-level tasks and clarify the gap between such a framework and a fully integrated mathematical foundation.