pith. sign in

arxiv: 2504.17041 · v2 · submitted 2025-04-23 · 🧮 math.LO · cs.CC

Feasibility of Primality in Bounded Arithmetic

Raheleh Jalali , Ond\v{r}ej Je\v{z}il This is my paper

Pith reviewed 2026-05-22 18:02 UTC · model grok-4.3

classification 🧮 math.LO cs.CC MSC 03F20
keywords AKS algorithmbounded arithmeticprimality testingVTC^0formal verificationnumber theorycyclotomic polynomialspolynomial division
0
0 comments X

The pith

The AKS primality algorithm is correct when formalized in the bounded arithmetic theory VTC^0_2.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper shows that the AKS algorithm for testing whether a number is prime can have its correctness established inside the weak bounded arithmetic theory VTC^0_2. The theory captures first-order statements provable from VTC^0 with the smash function and corresponds to limited counting resources. A sympathetic reader would care because it links a practical, deterministic polynomial-time algorithm directly to the foundations of feasible mathematics without needing stronger axioms. The authors first establish the result in S^1_2 plus iWPHP with two added algebraic axioms, then prove those axioms inside VTC^0_2 while supplying supporting formalizations of number theory and algebra in still weaker systems.

Core claim

We prove the correctness of the AKS algorithm within the bounded arithmetic theory T^{count}_2 or, equivalently, the first-order consequences of the theory VTC^0 expanded by the smash function, which we denote by VTC^0_2. Our approach initially demonstrates the correctness within the theory S^1_2 + iWPHP augmented by two algebraic axioms and then show that they are provable in VTC^0_2. The two axioms are: a generalized version of Fermat's Little Theorem and an axiom adding a new function symbol which injectively maps roots of polynomials over a definable finite field to numbers bounded by the degree of the given polynomial. To obtain our main result, we also give new formalizations of parts:

What carries the argument

The two algebraic axioms (generalized Fermat's Little Theorem and the injective root-mapping function for polynomials over definable finite fields) added to S^1_2 + iWPHP and then shown provable in VTC^0_2.

If this is right

  • Legendre's formula on the prime factorization of n! is provable in PV_1.
  • Key properties of the Combinatorial Number System and the existence of cyclotomic polynomials over Z/p hold in PV_1.
  • The inequality lcm(1,…,2n) ≥ 2^n is provable in S^1_2.
  • The Kung–Sieveking algorithm for polynomial division is correct when formalized in VTC^0.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This suggests that deterministic polynomial-time primality testing fits inside proof systems corresponding to very weak counting classes.
  • Similar formalizations might be attempted for other number-theoretic algorithms whose correctness is currently known only in stronger systems.
  • The work opens a route to studying the precise logical strength required for proving the correctness of practical primality tests.
  • One testable extension would be to check whether the same two axioms suffice for formalizing related algorithms such as Miller–Rabin variants inside the same theory.

Load-bearing premise

The generalized Fermat's Little Theorem and the injective root-mapping function for polynomial roots are both provable inside VTC^0_2.

What would settle it

An explicit small prime p and low-degree polynomial over the finite field Z/p for which either the generalized Fermat identity fails or no injective function mapping the roots to numbers below the degree exists.

read the original abstract

We prove the correctness of the AKS algorithm \cite{AKS} within the bounded arithmetic theory $T^{count}_2$ or, equivalently, the first-order consequences of the theory $VTC^0$ expanded by the smash function, which we denote by $VTC^0_2$. Our approach initially demonstrates the correctness within the theory $S^1_2 + iWPHP$ augmented by two algebraic axioms and then show that they are provable in $VTC^0_2$. The two axioms are: a generalized version of Fermat's Little Theorem and an axiom adding a new function symbol which injectively maps roots of polynomials over a definable finite field to numbers bounded by the degree of the given polynomial. To obtain our main result, we also give new formalizations of parts of number theory and algebra: $\bullet$ In $PV_1$: We formalize Legendre's Formula on the prime factorization of $n!$, key properties of the Combinatorial Number System and the existence of cyclotomic polynomials over the finite fields $\mathbb{Z}/p$. $\bullet$ In $S^1_2$: We prove the inequality $lcm(1,\dots, 2n) \geq 2^n$. $\bullet$ In $VTC^0$: We verify the correctness of the Kung--Sieveking algorithm for polynomial division.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The manuscript claims to prove the correctness of the AKS primality algorithm inside the bounded arithmetic theory T^{count}_2 (equivalently, the first-order consequences of VTC^0 expanded by the smash function, denoted VTC^0_2). The argument first establishes correctness inside the stronger theory S^1_2 + iWPHP augmented by two algebraic axioms—a generalized Fermat Little Theorem and an axiom introducing a new function symbol for an injective mapping of roots of polynomials over a definable finite field to {0,…,deg-1}—and then shows that both added axioms are theorems of VTC^0_2. Supporting formalizations are supplied: Legendre’s formula, the combinatorial number system, and cyclotomic polynomials over Z/p in PV_1; the inequality lcm(1,…,2n) ≥ 2^n in S^1_2; and the Kung–Sieveking polynomial-division algorithm in VTC^0.

Significance. If the central reduction holds, the result would be a notable contribution to bounded arithmetic and proof complexity by placing a non-trivial number-theoretic algorithm inside a comparatively weak theory. The explicit formalizations of Legendre’s formula, the combinatorial number system, and Kung–Sieveking division inside the indicated base theories constitute reusable technical assets that strengthen the manuscript.

major comments (1)
  1. [Abstract (approach paragraph)] Abstract (paragraph beginning 'Our approach initially demonstrates...'): The claim that the two algebraic axioms are provable inside VTC^0_2 is load-bearing for the equivalence to T^{count}_2. The manuscript must exhibit the precise derivations (or cite the relevant lemmas) showing that the generalized Fermat Little Theorem and the injective root-mapping function can be established in VTC^0_2 without hidden appeals to Σ_1^b-induction or counting principles stronger than those available in VTC^0_2.
minor comments (1)
  1. Clarify the exact syntactic status of the new function symbol introduced by the second algebraic axiom (its bounding term and how it is used in the language of VTC^0_2).

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading, the positive assessment of the technical contributions, and the recommendation for major revision. We address the single major comment below.

read point-by-point responses

  1. Referee: [Abstract (approach paragraph)] Abstract (paragraph beginning 'Our approach initially demonstrates...'): The claim that the two algebraic axioms are provable inside VTC^0_2 is load-bearing for the equivalence to T^{count}_2. The manuscript must exhibit the precise derivations (or cite the relevant lemmas) showing that the generalized Fermat Little Theorem and the injective root-mapping function can be established in VTC^0_2 without hidden appeals to Σ_1^b-induction or counting principles stronger than those available in VTC^0_2.

    Authors: We agree that the abstract is concise and that explicit pointers to the derivations strengthen the load-bearing claim. The manuscript already contains the required proofs without stronger induction or counting: the generalized Fermat Little Theorem is derived as Theorem 4.15 from the cyclotomic polynomials formalized in PV_1 (Lemma 3.8) together with order properties proved using only VTC^0 resources; the injective root-mapping function is constructed and shown to satisfy the required injectivity in Lemma 5.4, which invokes the Kung–Sieveking division algorithm formalized in VTC^0 (Theorem 2.12) and the lcm lower bound proved in S^1_2. Both arguments stay within the induction and counting strength of VTC^0_2. To make this transparent, we will revise the abstract to cite these specific results and add a short clarifying sentence in the approach paragraph. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation proceeds via independent formalizations

full rationale

The paper first establishes AKS correctness inside the stronger theory S^1_2 + iWPHP plus two added algebraic axioms (generalized Fermat and injective root mapping), then separately shows both axioms are theorems of the target VTC^0_2 by supplying explicit formalizations: Legendre formula and combinatorial number system in PV_1, lcm(1..2n) >= 2^n in S^1_2, and Kung-Sieveking division in VTC^0. These steps are self-contained against external number-theoretic benchmarks and do not reduce the final claim to any fitted parameter, self-citation chain, or definitional equivalence; the lifting of the axioms supplies independent content rather than importing the result by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claim rests on two ad-hoc algebraic axioms that are introduced in S^1_2 + iWPHP and later shown to be theorems of VTC^0_2; no free parameters are introduced and the supporting number-theoretic results are formalized rather than postulated.

axioms (2)
  • ad hoc to paper Generalized version of Fermat's Little Theorem
    Added to S^1_2 + iWPHP to establish AKS correctness before being proved inside VTC^0_2
  • ad hoc to paper Axiom introducing a new function symbol that injectively maps roots of polynomials over a definable finite field to numbers bounded by the degree
    Added to handle algebraic structure in the proof and later shown provable in VTC^0_2
invented entities (1)
  • New function symbol for injective mapping of polynomial roots no independent evidence
    purpose: To provide an injective map from roots of polynomials over finite fields to numbers up to the polynomial degree
    Postulated as an axiom in S^1_2 + iWPHP; independent evidence is the later proof that it is derivable in VTC^0_2

pith-pipeline@v0.9.0 · 5786 in / 1687 out tokens · 88201 ms · 2026-05-22T18:02:42.919751+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

20 extracted references · 20 canonical work pages

  1. [1]

    PRIMES is in P

    Manindra Agrawal, Neeraj Kayal, and Nitin Saxena. PRIMES is in P. Annals of mathematics, pages 781–793, 2004

    work page 2004

  2. [2]

    Feasibly Constructive Proof of Schwartz–Zippel Lemma and the Complexity of Finding Hitting Sets

    Albert Atserias and Iddo Tzameret. Feasibly Constructive Proof of Schwartz–Zippel Lemma and the Complexity of Finding Hitting Sets. InProceedings of the 57th Annual ACM Symposium on Theory of Com- puting, pages 1096–1107, 2025

    work page 2025

  3. [3]

    Buss.Bounded Arithmetic

    Samuel R. Buss.Bounded Arithmetic. PhD thesis, Princeton University, 1985

    work page 1985

  4. [4]

    Reverse mathematics of com- plexity lower bounds

    Lijie Chen, Jiatu Li, and Igor C Oliveira. Reverse mathematics of com- plexity lower bounds. In2024 IEEE 65th Annual Symposium on Foun- dations of Computer Science (FOCS), pages 505–527. IEEE, 2024

    work page 2024

  5. [5]

    Polynomial-time pseudodeterministic construction of primes

    Lijie Chen, Zhenjian Lu, Igor C Oliveira, Hanlin Ren, and Rahul San- thanam. Polynomial-time pseudodeterministic construction of primes. In2023 IEEE 64th Annual Symposium on Foundations of Computer Science (FOCS), pages 1261–1270. IEEE, 2023

    work page 2023

  6. [6]

    Cambridge University Press Cambridge, 2010

    Stephen Cook and Phuong Nguyen.Logical foundations of proof com- plexity, volume 11. Cambridge University Press Cambridge, 2010. 60

    work page 2010

  7. [7]

    Stephen A. Cook. Feasibly constructive proofs and the propositional calculus (preliminary version). InProceedings of the Seventh Annual ACM Symposium on Theory of Computing, STOC ’75, page 83–97, New York, NY, USA, 1975. Association for Computing Machinery

    work page 1975

  8. [8]

    Proof complexity of universal algebra in a csp dichotomy proof.arXiv preprint arXiv:2403.06704, 2024

    Azza Gaysin. Proof complexity of universal algebra in a csp dichotomy proof.arXiv preprint arXiv:2403.06704, 2024

    work page arXiv 2024

  9. [9]

    Constant-depth circuits for arith- metic in finite fields of characteristic two

    Alexander Healy and Emanuele Viola. Constant-depth circuits for arith- metic in finite fields of characteristic two. InAnnual Symposium on The- oretical Aspects of Computer Science, pages 672–683. Springer, 2006

    work page 2006

  10. [10]

    PhD thesis, Ph

    Emil Jeˇ r´ abek.Weak pigeonhole principle, and randomized computation. PhD thesis, Ph. D. thesis, Faculty of Mathematics and Physics, Charles University, Prague, 2005

    work page 2005

  11. [11]

    Abelian groups and quadratic residues in weak arithmetic

    Emil Jeˇ r´ abek. Abelian groups and quadratic residues in weak arithmetic. Mathematical Logic Quarterly, 56(3):262–278, 2010

    work page 2010

  12. [12]

    Iterated multiplication in VTC0.Archive for Mathemat- ical Logic, 61(5):705–767, 2022

    Emil Jeˇ r´ abek. Iterated multiplication in VTC0.Archive for Mathemat- ical Logic, 61(5):705–767, 2022

    work page 2022

  13. [13]

    Dual weak pigeonhole principle, boolean complexity, and derandomization.Annals of Pure and Applied Logic, 129(1-3):1– 37, 2004

    Emil Jeˇ r´ abek. Dual weak pigeonhole principle, boolean complexity, and derandomization.Annals of Pure and Applied Logic, 129(1-3):1– 37, 2004

    work page 2004

  14. [14]

    Prime Factorization in Models of PV1, 2025

    Ondˇ rej Jeˇ zil. Prime Factorization in Models of PV1, 2025

    work page 2025

  15. [15]

    Cambridge University Press, 1995

    Jan Kraj´ ıˇ cek.Bounded arithmetic, propositional logic and complexity theory, volume 60. Cambridge University Press, 1995

    work page 1995

  16. [16]

    Bounded arithmetic and the polynomial hierarchy.Annals of pure and applied logic, 52(1-2), 1991

    Jan Kraj´ ıˇ cek, Pavel Pudl´ ak, and Gaisi Takeuti. Bounded arithmetic and the polynomial hierarchy.Annals of pure and applied logic, 52(1-2), 1991

    work page 1991

  17. [17]

    Feasibly constructive proofs of suc- cinct weak circuit lower bounds.Annals of Pure and Applied Logic, 171(2):102735, 2020

    Moritz M¨ uller and J´ an Pich. Feasibly constructive proofs of suc- cinct weak circuit lower bounds.Annals of Pure and Applied Logic, 171(2):102735, 2020

    work page 2020

  18. [18]

    Phuong Nguyen.Bounded reverse mathematics. 2008

    work page 2008

  19. [19]

    Meta-Mathematics of Computational Complexity The- ory.ACM SIGACT News, 56(1):41–68, 2025

    Igor C Oliveira. Meta-Mathematics of Computational Complexity The- ory.ACM SIGACT News, 56(1):41–68, 2025. 61

    work page 2025

  20. [20]

    Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic.Logical Methods in Computer Science, 11, 2015

    J´ an Pich. Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic.Logical Methods in Computer Science, 11, 2015. 62

    work page 2015