AI-Assisted Mathematical Formalization: Engineering Workflow and Real-World Limits

What Is Formal Proof?

Traditional mathematical proofs rely on natural language and the reader’s understanding. Authors often omit obvious steps and present only the key arguments, allowing experienced readers to fill in the gaps. This makes proofs efficient to write, but it can also hide assumptions.

A formal proof requires every definition, assumption, lemma, and deduction to follow a strict set of rules and be checked step by step by a computer. Proof assistants such as Lean, Coq, and Isabelle verify types, dependencies, and inference rules. If even one required premise is missing, the check fails.

The main benefit of formalization is certainty. A proof that passes the checker is valid under the specified axioms and dependencies. The cost is the amount of work involved. Even a moderately difficult mathematical result may require a large body of foundational material to be formalized before work on the target theorem can begin.

The Claim of Formalizing Fermat’s Last Theorem in About 30 Hours

Recent reports have suggested that a highly capable AI model completed the formalization of Fermat’s Last Theorem in roughly 30 hours. This claim should be treated cautiously.

Publicly available information often does not answer several important questions:

• Did the formalization cover the complete theorem or only part of the task?
• How much existing mathematical library content did the project rely on, and did that library already contain relevant theory?
• Which proof assistant, library version, and checker version were used?
• What role did humans play, such as decomposing the task, correcting code, or designing the theorem statement?
• Was the result independently reviewed, and is there a public repository that allows reproduction?

Without this information, “30 hours” should be regarded as an unverified reported figure. It cannot, by itself, serve as a reliable measure of an AI system’s formalization capability.

Why Formalizing Fermat’s Last Theorem Is Difficult

Fermat’s Last Theorem cannot be adequately explained in just a few pages. Andrew Wiles’s proof depends on a long chain of mathematical theories. In broad terms, the argument assumes that a counterexample exists, maps it to an elliptic curve known as the Frey curve, uses Ribet’s theorem to connect that curve with modular forms, and finally derives a contradiction from the modularity theorem.

This chain involves several fields, including algebraic number theory, elliptic curves, modular forms, and Galois representations. To formalize the proof, a proof assistant must first have precise definitions and usable properties for these objects.

For example, the community-maintained Mathlib library for Lean contains a substantial amount of mathematical knowledge, but significant work remains before all the theory required for a complete formalization is available.

The public Lean formalization project led by Kevin Buzzard illustrates this challenge. Projects of this kind are planned on a timescale of years and require collaboration among multiple contributors. The main difficulty of complete formalization therefore lies in infrastructure and project organization, not merely in the difficulty of a single reasoning step.

The Hard Part Is Often the Premises, Not the Final Step

Natural-language theorem statements frequently omit conditions. For Fermat’s Last Theorem, a Lean statement must make details such as the following explicit:

theorem fermat_last (n : ℕ) (hn : 2 < n) (x y z : ℤ)
    (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) :
    x ^ n + y ^ n ≠ z ^ n

In this statement, the type and range of the exponent n must be explicit. It must also be clear whether the variables are integers or positive integers. Whether nonzero conditions are necessary must be decided as well. Each choice affects which tools and lemmas are available later in the proof.

The most common formalization errors are not syntax errors. They are mismatches between the formal statement and the intended mathematical meaning. For example, if the variable range is made too narrow, the resulting theorem may be true only for a special case. The checker can accept such a proof, but it will not answer the original question. Human review is therefore necessary.

What Role Does AI Play in the Workflow?

In a formalization project, AI is better understood as a continuously working engineering assistant than as a simple answer generator. It can typically help with the following tasks:

• Breaking a natural-language goal into types, assumptions, intermediate propositions, and a final conclusion;
• Determining which existing lemmas can be reused and which require new proofs;
• Writing formal code and handling details involving quantifiers, mappings, recursion, and type conversions;
• Locating problems from checker error messages and modifying local parts of the code;
• Switching to alternative strategies, such as proof by contradiction, reduction, or case analysis, when a direct proof fails.

AI’s main advantage is iteration speed. After each change, the proof assistant provides immediate feedback, allowing the model to adjust quickly. However, generated content may pass the checker while still failing to match the intended semantics. AI output therefore remains subject to human review.

A Reliable Six-Stage Workflow

1. Define the Scope

First, fix the exact version of the theorem. Specify the variable types, input ranges, and form of the conclusion. Do not send a natural-language title directly to a model. Break it into smaller, testable goals instead.

2. Build a Dependency Graph

Divide the proof into foundational definitions, general lemmas, key reductions, and the final conclusion. Record the prerequisites for each module. A dependency graph helps the team quickly identify where a failure occurs.

3. Prove Small Lemmas First

Exponent reductions, divisibility relationships, coprimality properties, and boundary conditions are good candidates for independent verification. The clearer these small lemmas are, the more stable the final composition will be.

4. Commit Incrementally and Check Immediately

Make only small changes at a time and run the formal checker immediately. This makes it easier to associate an error with the latest modification. If hundreds of lines are generated in one batch, it becomes difficult to determine whether a failure comes from logic, syntax, or a missing dependency.

5. Perform an Independent Review

Even when the formal check passes, review the proof structure and confirm that it meets the project’s objective. The specific review areas are described in the next section.

6. Use Continuous Integration

Proof files, dependency versions, checking scripts, and test examples should be managed together. Run the complete verification process after every change. This is similar to builds and regression testing in large software projects.

A Checklist for Auditing Theorem Statements

Formal checking guarantees only that a proof is valid under the supplied rules. An audit must determine whether those rules accurately represent the intended problem. Review the following items:

• Quantifier scope: Are variables restricted to the correct types and sets?
• Assumption strength: Has the statement quietly added stronger premises than the original problem?
• Boundary cases: Are zero, one, negative values, and the smallest exponent handled correctly?
• Circular reasoning: Has the conclusion been included among the assumptions?
• External facts: Does the proof rely on undocumented axioms or library theorems that have not been established?
• Opaque automation: Can people understand large automated search steps, and is their role clear?

After the audit, document the assumptions and dependencies so that other readers can review them.

How to Verify Reports About Formalization Results

When evaluating a report claiming that a formalization was completed in a few dozen hours, use the following process:

1. Find the original source, such as a paper, code repository, or project page, rather than relying on secondary reporting.
2. Confirm the publication date and record the library and tool versions used at that time.
3. Clarify the task definition: was it the complete theorem or only a subtask?
4. Examine the dependencies and determine how much existing library content contributed to the result.
5. Check for an independent reproduction or an assessment by experts in the relevant community.
6. Distinguish between “passed machine verification” and “accepted by the mathematical community.”

Only after these checks can the reported time figure be interpreted meaningfully.

Implications for Software Development and Research

The core practices of formalization—composable definitions, automated checking, and incremental modification—also apply to software engineering and research. Useful practices include:

• Writing checkable specifications for critical functions, including type constraints, preconditions, and postconditions;
• Requiring AI-generated code to pass compilation, tests, and static analysis before it enters a codebase;
• Clearly documenting assumptions and applicable boundaries for high-risk components such as financial calculations and cryptographic protocols;
• Storing verified components in reusable libraries to reduce duplicated work;
• Publishing both machine-checkable artifacts and human-readable explanations.

The value of formalization lies in making assumptions and dependencies visible. AI can accelerate this process, but determining whether a theorem statement is correct still requires people with relevant domain expertise.