Feasibility of Primality in Bounded Arithmetic

This paper establishes the correctness of the AKS primality test within the bounded arithmetic theory $T^{count}_2$ (equivalently $VTC^0_2$) by proving its validity in $S^1_2 + iWPHP$ under two algebraic axioms and demonstrating that these axioms, along with new formalizations of key number-theoretic and algebraic results, are provable in $VTC^0_2$.

The Gist

The Big Picture: The "Feasible" Proof

Imagine you have a massive library of mathematical truths. Some truths are easy to prove; others are so complex that proving them would take longer than the age of the universe, even with the fastest supercomputer.

In 2002, mathematicians discovered the AKS algorithm, a magical recipe that can tell you if a number is "Prime" (like 7 or 13) or "Composite" (like 8 or 15) very quickly. It's like having a super-fast metal detector that never makes a mistake.

But here is the puzzle: Just because we have a fast machine that works, does that mean we have a fast proof that the machine works?

This paper asks: Can we prove the AKS algorithm is correct using only "feasible" logic? In the world of math, "feasible" usually means a proof that doesn't require infinite resources or impossible calculations. The authors, Raheleh Jalali and Ondřej Ježil, say Yes. They managed to fit the entire proof of the AKS algorithm into a very strict, "lean" logical system called $VTC_0^2$.

Think of it like this: They took a giant, complex architectural blueprint (the AKS proof) and showed that it can be built using only simple, pre-fabricated bricks (basic arithmetic rules) without needing any heavy cranes or infinite supplies.

---

The Characters in Our Story

To understand how they did it, let's meet the cast of characters:

1. The AKS Algorithm (The Detective): A detective that checks if a number is prime. It's fast and reliable.
2. The Target System ($VTC_0^2$): This is the detective's office where the final proof lives. It is a very small, strict office. The detective here is very smart but has very limited tools. They can't use complex machinery; they can only use basic addition, multiplication, and simple counting. While this system is considered "weak" compared to the full power of standard mathematics, it is actually stronger than other systems often used for similar proofs (like $T_2$) when it comes to the specific types of statements needed here. It is the ultimate goal: proving the algorithm works within these tight constraints.
3. The "Magic Axioms" (GFLT and RUB): These are the special tools the authors had to invent to help the detective in the small office solve the case.

---

The Challenge: Why is this hard?

Proving the AKS algorithm is tricky because it relies on some deep algebraic tricks involving polynomials (equations with $X$'s) and roots (solutions to those equations).

Imagine the AKS algorithm is trying to prove a number is prime by checking if a giant, complex equation behaves a certain way.

• The Problem: In the "Lean" office, the detective is only allowed to look at small, simple equations. The AKS proof requires looking at huge, messy equations that the detective isn't allowed to see directly.
• The Analogy: It's like trying to prove a bridge is safe by looking at the microscopic structure of the steel, but your eyesight is so weak you can only see the paint on the surface. You need a way to infer the strength of the steel without seeing it.

The Solution: Two New Tools

To make the proof work in the small office, the authors introduced two "Magic Axioms" (rules they added to the detective's rulebook).

1. The "Generalized Fermat's Little Theorem" (GFLT)

• What it is: A famous math rule (Fermat's Little Theorem) says that if you have a prime number, certain math patterns repeat in a very specific way. The AKS algorithm relies on a more complex version of this pattern.
• The Analogy: Imagine a clock. If you know the time is 12:00, you know that in 12 hours, it will be 12:00 again. This is a simple pattern. The AKS algorithm needs to know that if you have a "prime clock," a much more complex dance of numbers will always land back on the starting point.
• The Fix: The authors added a rule to the small office that says, "We accept that this complex dance works, even if we can't prove every single step of the dance right now." This allows the detective to skip the heavy lifting and assume the pattern holds.

2. The "Root Upper Bound" (RUB)

• What it is: In algebra, a polynomial of degree $N$ can have at most $N$ solutions (roots). The AKS proof needs to count these solutions to prove the number is prime.
• The Analogy: Imagine a garden with a fence. You know there are at most 5 flowers in the garden. The AKS proof needs to point to every single flower and say, "That's one, that's two..."
• The Problem: In the small office, the detective can't easily count the flowers if the garden is huge and the flowers are hidden in a complex maze.
• The Fix: The authors added a "Root Upper Bound" tool. This is like a magical map that instantly labels every flower in the garden with a number from 1 to 5. It doesn't tell you where the flowers are, but it guarantees that if you find a flower, you can give it a unique ID number, and you'll never run out of numbers. This allows the detective to count the "roots" of the equation without getting lost in the maze.

The Journey of the Proof

The authors didn't just throw these tools at the problem; they built a bridge step-by-step using a two-part strategy:

1. Step 1: The Modular Step ($S_1^2$ + Axioms): First, they showed that if you have a basic logical system ($S_1^2$) and you simply assume the two Magic Axioms (GFLT and RUB) are true, you can prove the AKS algorithm works. This step isolates the core logic of the AKS proof, showing exactly what extra rules are needed to make it work.
2. Step 2: The Consolidation Step ($VTC_0^2$): Then, they went to their target system, $VTC_0^2$. They proved that this system is actually strong enough to prove the Magic Axioms themselves are true.
   • They proved the "Generalized Fermat" rule using a clever counting trick (like counting how many times a number divides into a factorial).
   • They proved the "Root Upper Bound" rule by showing that you can algorithmically find and label the roots of these equations, just like sorting a deck of cards.

By connecting these dots, they showed that the "extra rules" needed for the proof are not just assumptions, but facts that the system $VTC_0^2$ can verify on its own.

The Grand Conclusion

By connecting these dots, the authors proved:
"The AKS algorithm is correct, and we can prove it using a very restricted, yet surprisingly powerful, logical system."

Why Does This Matter?

1. Trust in Math: It confirms that the AKS algorithm isn't just a "black box" that works by luck. It is built on rock-solid, fundamental logic that doesn't require infinite power.
2. Computer Science: It tells us that the complexity of proving primality is "feasible" in a very specific sense. It fits within the limits of what computers can reasonably handle, specifically within the Counting Hierarchy.
3. The "Reverse Mathematics" Game: This is part of a game where mathematicians try to find the absolute minimum amount of logic needed to prove a theorem. The authors found a very low floor for this proof, showing that primality testing is a very "natural" and "simple" concept in the grand scheme of math.

In a Nutshell

The authors took a complex, high-tech proof (AKS) and showed that it can be dismantled and rebuilt using only simple, pre-fabricated bricks. They first identified the exact extra bricks needed (GFLT and RUB) to make the proof work in a basic system, and then showed that their target system ($VTC_0^2$) is strong enough to manufacture those bricks itself.

A Note on "Feasibility": It is important to be nuanced here. The system $VTC_0^2$ is indeed very "weak" compared to the full power of standard mathematics. However, it is not exactly the same as "polynomial-time" reasoning (the strictest definition of feasible). Its complexity corresponds to the Counting Hierarchy, which is actually stronger than simple polynomial-time reasoning. So, while the proof is incredibly efficient and "lean" by the standards of mathematical logic, it still operates in a realm slightly more powerful than the absolute minimum for computer efficiency.

It's like proving that a skyscraper can be built using only a hammer and a saw, provided you have a very clever blueprint—and that blueprint is slightly more advanced than a basic hammer-and-saw kit, but still far simpler than a full construction crane.

Technical Summary

1. Problem Statement

The paper addresses the question of feasibility regarding the proof of primality testing. Specifically, it asks: How "feasible" (in terms of computational complexity) is a formal proof that the AKS primality test is correct?

While the AKS algorithm (Agrawal, Kayal, and Saxena, 2002) is the first deterministic polynomial-time algorithm for primality testing, its correctness proof relies on non-trivial number-theoretic and algebraic statements (e.g., properties of cyclotomic polynomials, Fermat's Little Theorem, and root counting). The authors aim to formalize this proof within bounded arithmetic, a field of proof complexity where theories correspond to specific complexity classes.

The core challenge is that standard bounded arithmetic theories (like $S^1_2$) are too weak to prove certain algebraic facts required by the AKS proof without additional axioms. The authors seek to determine the weakest theory capable of proving the correctness of the AKS algorithm, denoted as $\text{AKSCorrect}$.

2. Methodology

The authors employ a modular formalization strategy, breaking the AKS correctness proof into logical components and determining the minimal theory required for each part.

1. Decomposition of the AKS Proof: They restructure the original AKS proof into a sequence of lemmas (A through H) and identify the specific algebraic and number-theoretic tools required for each step.
2. Introduction of Auxiliary Axioms: To bridge the gap between weak theories and the requirements of the AKS proof, they introduce two specific algebraic axioms:
   • Generalized Fermat's Little Theorem (GFLT): A formalization stating that $(X+a)^p \equiv X^p + a \pmod{p, X^r-1}$ for specific parameters.
   • Root Upper Bound (RUB): An axiom introducing a function symbol $\iota$ that injectively maps the roots of a sparse polynomial to integers bounded by the polynomial's degree. This replaces the need to count roots explicitly, which is difficult in weak theories.
3. Formalization in Intermediate Theory: They first prove the correctness of AKS in the theory $S^1_2 + \text{iWPHP} + \text{RUB} + \text{GFLT}$. Here, $\text{iWPHP}$ is the injective weak pigeonhole principle. This intermediate theory represents the modular decomposition of the proof, isolating the "barebones" axioms necessary to derive the result.
4. Derivation in Stronger Theory: They then demonstrate that the theory $VTC^0_2$ (an extension of $VTC^0$ with the smash function and polynomial-time functions) proves the consequences of the intermediate theory. Specifically, $VTC^0_2$ proves that the axioms $\text{iWPHP}$, $\text{RUB}$, and $\text{GFLT}$ hold.
5. Technical Formalizations: The authors provide new formalizations of:
   • Legendre's Formula (for prime factorization of factorials) in $PV_1$.
   • Cyclotomic polynomials and extensions over finite fields in $PV_1$.
   • The Kung–Sieveking algorithm for polynomial division in $VTC^0$.

3. Key Contributions

A. Formalization of Algebraic Structures in Weak Theories

• Legendre's Formula: Proven in $PV_1$, establishing the exponent of a prime $p$ in $n!$. This is crucial for bounding the least common multiple (LCM) of numbers, a key step in proving the existence of the parameter $r$ in the AKS algorithm.
• Cyclotomic Polynomials: The authors prove the existence of cyclotomic extensions of finite fields $\mathbb{Z}/p\mathbb{Z}$ within $PV_1$. This allows the construction of the irreducible polynomial $h$ required for the "introspective" argument in the AKS proof.
• Polynomial Division: They verify the correctness of the Kung–Sieveking algorithm for dividing high-degree polynomials within $VTC^0$, a result of independent interest for bounded arithmetic.

B. The Root Upper Bound (RUB) Axiom

The paper introduces RUB as a novel axiom to handle sparse polynomials of arbitrary degree. Unlike previous attempts to formalize the Fundamental Theorem of Algebra (which only worked for small-degree polynomials), RUB provides an injective mapping from roots to indices. This axiom is essential for proving Lemma G (the upper bound on the size of the set of "introspective" polynomials) without requiring full counting capabilities.

C. Hierarchy of Theories

The authors establish the following logical chain:

1. $PV_1$: Formalizes basic algebraic structures and Legendre's formula.
2. $S^1_2 + \text{iWPHP} + \text{RUB} + \text{GFLT}$: Represents the modular decomposition of the proof, containing the specific axioms required to prove the correctness of the AKS algorithm.
3. $VTC^0_2$: As the encompassing theory, $VTC^0_2$ proves that the axioms used in the intermediate theory (specifically $\text{iWPHP}$, $\text{RUB}$, and $\text{GFLT}$) hold for $\Sigma^B_1$-definable functions. Consequently, $VTC^0_2$ proves the correctness of the AKS algorithm.
4. $T^{count}_2$: Since $VTC^0_2$ is conservative over $T^{count}_2$ for $\Sigma^B_1$ sentences, the result extends to $T^{count}_2$. Note that $VTC^0_2$ is stronger than $T^{count}_2$ regarding the $\Sigma^B_1$ statements relevant to this paper; it is not a weaker alternative but the theory that validates the axioms of the intermediate system.

4. Main Results

• Theorem: The theory $VTC^0_2$ (and equivalently $T^{count}_2$ for $\Sigma^B_1$ sentences) proves the sentence $\text{AKSCorrect}$.
  • $\text{AKSCorrect}$ is the statement: $\forall x (\text{Prime}(x) \leftrightarrow \text{AKSPrime}(x))$.
• Corollary: The correctness of the AKS algorithm is provable in a theory corresponding to the complexity class $TC^0$ (constant-depth threshold circuits) extended with polynomial-time functions.
• Specific Lemma Proofs:
  • Lemma C & D: Proven in $S^1_2$ using Legendre's formula to show that a suitable $r$ exists such that $\text{ord}_r(n) > \log^2 n$.
  • Lemma H: Proven in $S^1_2 + \text{iWPHP} + \text{RUB} + \text{GFLT}$ by showing that assuming $n$ is composite leads to a contradiction with the injective weak pigeonhole principle (iWPHP) via the composition of the functions from Lemma F and Lemma G.

5. Significance

• Bounded Reverse Mathematics: This work provides a deep insight into the intrinsic power of bounded arithmetic theories. It demonstrates that fundamental results in computational number theory (like the AKS proof) can be captured by theories corresponding to the counting hierarchy, provided specific algebraic axioms are available.
• Proof Complexity: The result has implications for propositional proof complexity. Since $VTC^0_2$ proves the correctness of AKS, there exists a specific propositional proof system (corresponding to $VTC^0_2$) where the tautologies expressing the correctness of AKS for inputs of various lengths can be efficiently proved.
• Witnessing and Algorithms: The formalization connects the provability of existential statements in bounded arithmetic to the existence of polynomial-time algorithms. While the paper notes that the witnessing for the factorization problem remains trivial, the formalization of the primality test itself is a significant step toward understanding the logical strength required for "feasible" mathematics.
• Algebraic Formalization: The paper advances the state of the art in formalizing algebra within bounded arithmetic, particularly regarding cyclotomic polynomials and sparse polynomials, which were previously untreated or only partially treated in this context.
• Complexity Caveat: It is important to note that $VTC^0_2$ corresponds to the counting hierarchy ($TC^0$ extended with polynomial-time functions), which is believed to be considerably stronger than strict polynomial-time reasoning ($P$). While $VTC^0_2$ is very weak by the standards of mathematical logic, it should not be characterized as a "feasible" system in the strict sense of polynomial-time computability. The question of whether the result can be pushed down to a truly feasible (polynomial-time) theory remains open.

Conclusion

Jalali and Ježil successfully prove that the correctness of the AKS primality test is a theorem of the bounded arithmetic theory $VTC^0_2$. By introducing the RUB axiom and formalizing key algebraic lemmas in $PV_1$ and $S^1_2$, they bridge the gap between the combinatorial nature of the AKS algorithm and the logical limitations of weak arithmetic theories. The proof is modularized within an intermediate theory ($S^1_2$ plus specific axioms), which is then shown to be fully contained within $VTC^0_2$. This establishes that primality testing is logically "feasible" within a theory corresponding to the counting hierarchy, though whether it resides in a strictly polynomial-time theory remains an open problem.