Complexity Theory

Motivation

Multiplying two $n$-bit integers is the basic operation underneath division, square roots, base conversion, evaluation of elementary functions to high precision, and polynomial and matrix arithmetic over $\mathbb Z$; the cost of all of these is usually quoted in units of the multiplication cost $\mathsf M(n)$. In 1971 Schönhage and Strassen proved $\mathsf M(n)=O(n\log n\log\log n)$ on a multitape Turing machine and conjectured that $n\log n$ is the true order of growth. The upper half of that conjecture was settled by Harvey and van der Hoeven in 2019 (published 2021), who gave an algorithm achieving $\mathsf M(n)=O(n\log n)$ in the same machine model.

Timeline (multitape Turing model).

• 1962–1971: Karatsuba ($O(n^{\log_2 3})$), Toom and Cook, Schönhage; then Schönhage–Strassen, $O(n\log n\log\log n)$, with the conjecture $\mathsf M(n)=\Theta(n\log n)$.
• 2007: Fürer, $O(n\log n\,K^{\log^* n})$ for an unspecified constant $K>1$.
• 2014–2018: Harvey, van der Hoeven and Lecerf make the constant explicit, reaching $O(n\log n\,4^{\log^* n})$.
• 2019/2021: Harvey and van der Hoeven, $O(n\log n)$, unconditionally (Theorem 1.1 of the paper below).
• 2026: an OpenAI preprint claims $O(n(\lg n)^{1-\kappa})$ with $\kappa=2^{-182}$, which uses the $O(n\log n)$ multiplier as a subroutine; that line of work is tracked in a separate mission.

Setting

A $k$-tape Turing machine, in the conventions of Montanaro's Computational Complexity lecture notes (§3, §3.4), has the following parts:

• a finite alphabet containing a blank $\square$ and a start symbol $\triangleright$;
• a finite set of states with a start state $\mathrm{START}$ and a distinct halting state $\mathrm{HALT}$;
• $k\ge2$ tapes: a read-only input tape, an output tape, and $k-2$ work tapes. Each tape is infinite in one direction, has its own head, and holds $\triangleright$ in its first cell and nowhere else.

In one step the machine reads the symbol under every head, writes a symbol under every head, moves each head by at most one cell (never left of $\triangleright$), and changes state. Once in $\mathrm{HALT}$ it stays there unchanged.

For a bit string $x\in\{0,1\}^n$, written most significant bit first, let $\operatorname{val}(x)$ be the integer it represents, and for $0\le z<2^k$ let $\operatorname{bin}_k(z)$ be the length-$k$ binary representation of $z$, padded with leading zeros. The machine is started in $\mathrm{START}$ with $\triangleright\,x\#y$ on the input tape. It computes the product if, for every $n\ge1$ and all $x,y\in\{0,1\}^n$, it reaches $\mathrm{HALT}$ with the output tape holding exactly $\triangleright\,\operatorname{bin}_{2n}(\operatorname{val}(x)\operatorname{val}(y))$ followed by blanks. Its running time $T(n)$ is the largest number of steps it takes on any pair of $n$-bit inputs. Write

Formalization targets

Goal: Theorem 1.1 of Harvey–van der Hoeven, as stated

There is one machine $M$ that computes the product and has running time

with $\log$ the natural logarithm. That is, $T(n)\le c\,n\log n$ for all $n\ge n_0$, for some constants $c>0$ and $n_0$.

Milestones

The milestones are the self-contained mathematical statements behind the Gaussian resampling step of the paper (§4.1–§4.2) and its prime-selection step (§5.2):

1. Theorem 4.2 (resampling identity). For coprime $1\le s<t$ and $\alpha>0$, the resampling maps $\mathcal S,\mathcal T:\mathbb C^s\to\mathbb C^t$ and the permutations $\mathcal P_s,\mathcal P_t$ satisfy $\mathcal T\mathcal P_s\mathcal F_s=\mathcal P_t\mathcal F_t\mathcal S$, where $\mathcal F_n$ is the normalized DFT of length $n$.
2. Lemma 4.5. $\|\mathcal S\|<1+\alpha^{-1}$ in the operator norm for the supremum norms.
3. Lemma 4.6. If $\alpha^2\theta\ge1$, where $\theta=t/s-1$, then $\|\mathcal E\|<2.01\,e^{-\pi\alpha^2\theta/2}<2^{-\alpha^2\theta}$, where $\mathcal E=\mathcal C\mathcal T\mathcal D-\mathcal I$ is the normalized square system of §4.2.
4. Lemma 5.1. For $\eta\in(0,\tfrac14)$ and $x\ge e^{2/\eta}$, there are at least $\tfrac12\eta x/\log x$ primes in $\big((1-2\eta)x,(1-\eta)x\big]$.
5. Theorem 1.1 in the $\kappa$-framework, $\mathrm{KappaBound}(0)$. The same machine statement with running time $O(n\lg n)$, where $\lg n=\max(\lceil\log_2 n\rceil,1)$. This is the $\kappa=0$ member of the family $O(n(\lg n)^{1-\kappa})$ studied in the companion mission. It is equivalent to the goal, because $\log n$ and $\lg n$ differ by at most a constant factor for $n\ge2$.

Significance

The result. Theorem 1.1 makes $n\log n$ an unconditional upper bound for integer multiplication on multitape Turing machines, matching the Schönhage–Strassen conjecture. Through standard Newton-iteration reductions it gives the same bound for division and $k$-th roots, and $O(n\log^2 n)$ for computing elementary constants and functions to precision $n$. No superlinear lower bound for $\mathsf M(n)$ is known, so the matching lower bound remains open.

Formalizing it. The theorem has a published proof but no machine-checked proof. A formal proof would also check the full chain of reductions (splitting into digits, Chinese-remainder multidimensional convolution, Gaussian resampling, Nussbaumer polynomial transforms, fixed-point error control, and Turing-machine data movement), each with explicit error and cost accounting. The resampling identity and the norm bounds are statements of independent interest in discrete harmonic analysis, and are useful to formalize on their own.

Difficulty

The obvious approach is a Fourier transform over $\mathbb C$ with $\Theta(\log n)$ bits of precision. This leads to recursive estimates of the form $\mathsf M(n)=O(n\,\mathsf M(\log n))+O(n\log n)$, and every such scheme loses a factor that tends to infinity at each level of recursion. Reaching $O(n\log n)$ requires every level of recursion to cost a constant factor less than the previous one. That in turn requires transforms of prime length to be replaced by power-of-two transforms at essentially no extra cost, while keeping $O(1)$ bits of precision loss per level. In the Turing model, every reshuffling of data also costs time proportional to the data volume times a logarithm, so the reductions must avoid general sorting wherever its cost would dominate.

Formalization scope

• Machine model. Every target uses one shared definition file, IntMul_MultitapeModel, which follows the $k$-tape conventions of Montanaro's lecture notes. Tapes are indexed by $\mathbb N$ and begin with $\triangleright$. There is a designated $\mathrm{HALT}$ state that freezes the configuration. Tape $0$ is a read-only input tape and tape $1$ is the output tape. The input is $\triangleright\,x\#y$, and the output tape must hold exactly $\triangleright$ followed by the product bits and then blanks. Running time is the number of steps until $\mathrm{HALT}$.
• The bound. As in the notes' definition of $O(\cdot)$: there are $c>0$ and $n_0$ with $T(n)\le c\,g(n)$ for $n\ge n_0$, and correctness is required for every $n\ge1$. Following the papers, $n$ is the length of each operand and only well-formed inputs $x\#y$ are constrained.
• Logarithms. The goal uses the paper's natural logarithm, so any valid threshold has $n_0\ge2$, because $\log1=0$. Milestone 5 restates the goal with $\lg n=\max(\lceil\log_2n\rceil,1)$, the convention shared with the companion mission.
• No trivial solutions. A machine that never halts, or that halts with the wrong output, on any well-formed input does not satisfy the definition, and the constant $c$ must be positive.
• Resampling maps. Vectors in $\mathbb C^n$ are functions on $\mathbb Z/n\mathbb Z$, which encodes the paper's convention that an index is read mod $n$. Norms are supremum norms, as in §2.2 of the paper. The paper's sums over $j\in\mathbb Z$ are written as matrices whose entries are lattice sums over each residue class. The definitions are in IntMul_HvdH_Resampling.
• Infrastructure needed: multidimensional DFT and convolution identities, Gaussian and theta-function estimates, Chebyshev-function bounds, a library of Turing-machine subroutines (sorting, matrix transposition, fixed-point arithmetic) with cost bounds, and a composition calculus for machines. The machine library and the cost calculus can be reused across every complexity mission on the platform.

Selected references

• D. Harvey, J. van der Hoeven, Integer multiplication in time $O(n\log n)$, Annals of Mathematics 193(2), 563–617, 2021. https://doi.org/10.4007/annals.2021.193.2.4 (preprint: https://hal.science/hal-02070778)
• A. Schönhage, V. Strassen, Schnelle Multiplikation großer Zahlen, Computing 7, 281–292, 1971. https://doi.org/10.1007/BF02242355
• M. Fürer, Faster integer multiplication, SIAM Journal on Computing 39(3), 979–1005, 2009. https://doi.org/10.1137/070711761
• D. Harvey, J. van der Hoeven, G. Lecerf, Even faster integer multiplication, Journal of Complexity 36, 1–30, 2016. https://doi.org/10.1016/j.jco.2016.03.001
• J. B. Rosser, L. Schoenfeld, Approximate formulas for some functions of prime numbers, Illinois Journal of Mathematics 6, 64–94, 1962. https://doi.org/10.1215/ijm/1255631807
• Wikipedia, Multiplication algorithm. https://en.wikipedia.org/wiki/Multiplication_algorithm

Motivation

Machine scheduling asks how to assign jobs to machines over time. In many applications a job also needs additional scarce resources while it runs: a tool, a skilled operator, a memory bank, a channel. Adding such resources can turn a problem with a polynomial algorithm into an NP-hard one. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the standard three-field classification $\alpha\,|\,\beta\,|\,\gamma$ of scheduling problems (Graham, Lawler, Lenstra and Rinnooy Kan 1979) with a resource field $res\lambda\sigma\rho$. They then drew the complete borderline between easy and hard problems for unit-time jobs, identical or uniform machines and the makespan criterion. Their Fig. 2 marks each problem type as polynomially solvable or NP-hard.

This mission formalizes the two hardness results of that classification that come from graph partition problems (Theorems 2 and 3, p. 15). Two identical machines are easy under any resource constraints (Theorem 1, after Garey and Johnson 1975). Theorems 2 and 3 show that a third identical machine, or two machines of different speeds, already makes the problem strongly NP-hard, once the number of unit resources is part of the input.

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines $M_1,\dots,M_m$. Each machine processes at most one job at a time, and each job runs on one machine without interruption. Machine $M_i$ has a speed $q_i>0$, and every job has unit execution requirement $p_j=1$, so it takes time $1/q_i$ on $M_i$. Identical machines ($P$) are the case $q_i=1$; uniform machines ($Q$) allow arbitrary speeds.

There are $l$ resources $R_1,\dots,R_l$. Resource $R_h$ has a positive integer size $s_h$, the amount available at any time. Job $J_j$ needs a nonnegative integer amount $r_{hj}$ of $R_h$ throughout its execution. A schedule assigns each job a machine $\mu(j)$ and a start time $S_j\ge 0$. Its completion time is $C_j=S_j+1/q_{\mu(j)}$, and it is being executed at every time $t$ with $S_j\le t<C_j$. A schedule is feasible when:

• jobs on the same machine do not overlap in time;
• at every time $t$, the set $S_t$ of jobs being executed satisfies

The makespan is $C_{\max}=\max_j C_j$.

The resource type $res{\cdot}11$ means three things: the number $l$ of resources is part of the input, every size is $s_h=1$, and every requirement satisfies $r_{hj}\le1$. A unit resource is therefore a conflict: two jobs that both need it can never run at the same time. The problems here have no precedence constraints. $Pm\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ and $Qm\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ ask for a feasible schedule of minimum makespan. Their decision versions ask, for a threshold $y$, whether a feasible schedule with $C_{\max}\le y$ exists.

The source problems are two graph problems on a graph $G=(V,E)$ with $|V|=3t$:

• PARTITION INTO TRIANGLES: can $V$ be partitioned into $t$ triples of pairwise adjacent vertices?
• PARTITION INTO PATHS OF LENGTH 2: can $V$ be partitioned into $t$ triples, each with at most one nonadjacent pair, that is, each spanning a path of length 2?

Both are NP-complete (Garey and Johnson 1979, problems GT11 and GT13).

The construction of p. 15 introduces one job per vertex and one unit resource $R_{\{j,k\}}$ per nonadjacent pair $\{j,k\}$, required by $J_j$ and $J_k$ only.

Formalization targets

Goal: Theorem 3

Formally: if the language of PARTITION INTO PATHS OF LENGTH 2 is NP-hard, then the language of unary codes of yes-instances of the decision version of $Q2\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ is NP-hard. The two speeds are arbitrary positive integers.

Milestones

1. The construction's key property (p. 15). In the constructed instance, two distinct jobs can be executed simultaneously if and only if their vertices are adjacent.
2. The triangle equivalence (proof of Theorem 2). $G$ has a partition into triangles if and only if the constructed instance on three identical machines has a feasible schedule with $C_{\max}\le t$.
3. Theorem 2. $P3\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ is NP-hard in the strong sense, given the NP-hardness of PARTITION INTO TRIANGLES.
4. The paths equivalence (proof of Theorem 3). $G$ has a partition into paths of length 2 if and only if the constructed instance on two uniform machines with speeds $q_1=2$, $q_2=1$ has a feasible schedule with $C_{\max}\le t$.

Significance

The results. Theorems 2 and 3 are two of the minimal NP-hard problems in the paper's classification. Together with Theorem 1 they place the borderline exactly: with unit resources whose number is part of the input, two identical machines are polynomial, while three identical machines, or two machines of different speeds, are strongly NP-hard. Strong NP-hardness rules out pseudo-polynomial algorithms unless P = NP, and it carries over to every more general resource type and machine environment in Fig. 1 and Fig. 2. Section 4.1 of the paper also derives hardness for $\sum C_j$ and $L_{\max}$ from these instances.

Formalizing it. The results are classical and proved on paper, but the paper's proofs are one sentence each ("Clearly", "It is easily seen"). No machine-checked proof exists, and the platform has no model of resource-constrained scheduling with real-valued time. This mission produces that model. It also produces a precise statement of strong NP-hardness on top of Cook's Turing-machine definitions, and the first formal NP-hardness reductions from graph partition problems to scheduling.

Difficulty

The scheduling half of each equivalence depends on the real-time model. On two uniform machines of speeds 2 and 1, jobs take time $\tfrac12$ and $1$, so jobs on the fast machine start at half-integers or anywhere else. The resource constraint must hold at every real time, not at a finite set of checkpoints. An argument that treats time as integer slots applies to the triangle case but does not transfer to the paths case.

The complexity half needs polynomial-time computability of the construction on Cook's one-tape Turing machines, on encoded strings that include malformed inputs. It also needs closure of polynomial-time reductions under composition, which the imported complexity layer states but does not prove.

Formalization scope

• Time and schedules. Start times are nonnegative reals, execution intervals are half-open $[S_j,C_j)$, and the resource constraints are imposed at every real time. Schedules are nonpreemptive.
• Indices. Jobs, machines and resources are 0-based (Fin n, Fin m, Fin l), so $q_1,q_2$ are q 0, q 1.
• Decision versions. "NP-hard" refers to the decision version with a threshold $y$. Thresholds are natural numbers and the $Q2$ speeds are positive integers. This restricted problem is a subproblem of the one with rational data, so its hardness is the stronger statement.
• Encodings and strong NP-hardness. Instances are strings over a two-letter alphabet with every number in unary. Graphs are $t$ in unary followed by the $3t\times 3t$ adjacency matrix, so $|V|=3t$ is part of the instance. Languages contain only codes of yes-instances. Strong NP-hardness is NP-hardness of the unary code language. With unary numbers, $\mathrm{Max}(I)\le\mathrm{Length}(I)$, so this is equivalent to Garey and Johnson's definition. The complexity layer is the published module CookPvsNP_defs.
• Cited hypothesis. Each hardness theorem takes as its only hypothesis the NP-hardness of its source problem, which the paper cites from Garey and Johnson rather than proves. The hypothesis is a true statement about a nonempty, non-universal language. The statements are not weakened to a reduction between languages, and they assume nothing about P versus NP.
• Source problems. The paper's phrase "three vertices, at most two of which are nonadjacent" is read as "at most one nonadjacent pair", which is Garey and Johnson's GT13. Reading it as "at most two nonadjacent pairs" would admit triples with a single edge and change the problem. PARTITION INTO PATHS OF LENGTH 2 reuses the published definition CubicP3Partition.P3Factor, a spanning non-induced $P_3$-factor.
• Construction. Resources are indexed by the nonadjacent pairs $j<k$ in lexicographic order, one per unordered pair and none for a pair $\{j,j\}$. A diagonal resource would make every job infeasible.
• Not trivial. A model that checks resources only at integer times, or only at start times, would make the paths equivalence false. A hypothesis on the target problem would make the goal circular. The definitions rule out both.

Welcome contributions: proofs of the two equivalences, polynomial-time computability of the construction on Cook's machines, and a general composition lemma for polynomial-time reductions. The composition lemma is reusable for every hardness mission built on CookPvsNP_defs.

Selected references

• J. Błażewicz, J. K. Lenstra, A. H. G. Rinnooy Kan, Scheduling subject to resource constraints: classification and complexity, Discrete Applied Mathematics 5 (1983) 11–24. https://doi.org/10.1016/0166-218X(83)90012-4
• M. R. Garey, D. S. Johnson, Complexity results for multiprocessor scheduling under resource constraints, SIAM Journal on Computing 4 (1975) 397–411. https://doi.org/10.1137/0204035
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, San Francisco, 1979, ISBN 0-7167-1045-5.
• R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• S. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problems. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

Motivation

Schönhage and Strassen conjectured in 1971 that $n\log n$ is the optimal order of growth for multiplying two $n$-bit integers on a multitape Turing machine. Harvey and van der Hoeven proved the matching upper bound $O(n\log n)$ (Annals of Mathematics, 2021). In September 2026, a preprint by OpenAI, Integer multiplication below $n\log n$, claimed that this bound can itself be beaten by a power of the logarithm, in the same model. If correct, the upper half of the conjecture's "$\Theta(n\log n)$" is false. Two independent follow-up projects then increased the exponent saving $\kappa$ by many orders of magnitude. This mission targets the strongest claimed saving and takes the earlier claims as milestones.

Timeline (multitape Turing model; all bounds are of the form $O(n(\lg n)^{1-\kappa})$).

• 2021: Harvey and van der Hoeven, $\kappa=0$, that is, $O(n\log n)$. Published and refereed.
• 23 September 2026: OpenAI preprint, $\kappa=2^{-182}$ (Theorem 1 of the preprint). The preprint has not been refereed.
• October 2026: D. Colkitt, integer-mult-bounds, a series of patches to the OpenAI manuscript with checked numerical certificates, reaching $\kappa=2^{-30}$. The project describes this as conditional on the OpenAI manuscript and as having had no independent review.
• October 2026: S. Jain, integer-mult-kappa, building on both, reaching $\kappa=3666565558019/10^{17}\approx3.67\times10^{-5}>2^{-15}$ ("round six"). It is also stated to be conditional and unreviewed. Its numerical certificate is checked by computation in the Lean kernel, but the analytic facts behind that certificate are taken as premises.

Setting

A $k$-tape Turing machine, in the conventions of Montanaro's Computational Complexity lecture notes (§3, §3.4), has the following parts:

• a finite alphabet containing a blank $\square$ and a start symbol $\triangleright$;
• a finite set of states with a start state $\mathrm{START}$ and a distinct halting state $\mathrm{HALT}$;
• $k\ge2$ tapes: a read-only input tape, an output tape, and $k-2$ work tapes. Each tape is infinite in one direction, has its own head, and holds $\triangleright$ in its first cell and nowhere else.

In one step the machine reads the symbol under every head, writes a symbol under every head, moves each head by at most one cell (never left of $\triangleright$), and changes state. Once in $\mathrm{HALT}$ it stays there unchanged.

For $x\in\{0,1\}^n$ (most significant bit first), $\operatorname{val}(x)$ is the integer that $x$ represents, and $\operatorname{bin}_k(z)$ is the length-$k$ binary representation of $z$. A machine computes the product if, for every $n\ge1$ and all $x,y\in\{0,1\}^n$, when started on input $\triangleright\,x\#y$ it reaches $\mathrm{HALT}$ with the output tape holding exactly $\triangleright\,\operatorname{bin}_{2n}(\operatorname{val}(x)\operatorname{val}(y))$ followed by blanks. Its running time $T(n)$ is the largest number of steps on any pair of $n$-bit inputs. With $\lg n=\max(\lceil\log_2n\rceil,1)$, define

Formalization targets

Goal

Milestones: the earlier, weaker bounds

1. $\mathrm{KappaBound}(0)$: Harvey–van der Hoeven, Theorem 1.1. This is stated as a milestone of the companion mission, in the same machine model, and is referenced here.
2. $\mathrm{KappaBound}(2^{-182})$: OpenAI, Theorem 1.
3. $\mathrm{KappaBound}(2^{-30})$: Colkitt's ternary five-subset checkpoint.

Each milestone is implied by the goal, because $(\lg n)^{1-\kappa}$ decreases in $\kappa$. Each one is also a published claim in its own right and a natural intermediate formalization target. The $\kappa=0$ and $\kappa=2^{-182}$ constructions are the ones that the later claims rely on.

Significance

The result. Any $\kappa>0$ shows that $n\log n$ is not the optimal running time for multitape machines, which refutes the upper half of the Schönhage–Strassen conjecture as usually stated. The OpenAI preprint also derives the same bound for exact division and integer square roots (its Corollary 2). Larger values of $\kappa$ quantify how far below $n\log n$ multiplication can go. The bound is a statement about growth rates, and the constants involved are astronomically large.

Formalizing it. None of the three positive-$\kappa$ results has been refereed, and the two follow-ups explicitly depend on the OpenAI manuscript. Their written arguments, their computer-checked combinatorial certificates (rank sums, moment bounds, rational margins), and the full multiplication theorem have not been formally verified. Machine-checking any of the milestones would be the first independent confirmation of the corresponding claim. A formal disproof, or a formal identification of a gap, would be equally informative.

Difficulty

Fourier-based multiplication scans $\Theta(n)$ stored bits at each of $\Theta(\log n)$ transform levels, so any algorithm that performs those levels one at a time pays $\Theta(n\log n)$ for data movement and arithmetic alone. Beating this requires both moving data and carrying out butterfly layers at cost $o(V\log n)$ on a tape that is accessed sequentially, where $V$ is the stored volume. In the preprint this is done with recursive linear networks whose total number of smaller calls is strictly less than (number of roles) × (arity). The follow-ups improve $\kappa$ by finding better networks and tighter parameter choices, all certified by large exact computations. Each claim therefore combines a long analytic argument, a Turing-machine implementation, and a finite certificate, and all three must be formalized.

Formalization scope

• Machine model. The definitions are in IntMul_MultitapeModel, shared with the Harvey–van der Hoeven mission, and follow the $k$-tape conventions of Montanaro's lecture notes. Tapes begin with $\triangleright$. There is a $\mathrm{HALT}$ state that freezes the configuration. Tape $0$ is a read-only input tape holding $\triangleright\,x\#y$, and tape $1$ is the output tape, which must hold exactly $\triangleright$, then the product bits, then blanks. Running time is the number of steps until $\mathrm{HALT}$.
• The bound. As in the notes' definition of $O(\cdot)$: there are $c>0$ and $n_0$ with $T(n)\le c\,n(\lg n)^{1-\kappa}$ for $n\ge n_0$, and correctness is required for every $n\ge1$. Following the papers, $n$ is the length of each operand. The exponent $1-\kappa$ is a real power of a number that is at least $1$.
• No trivial solutions. A machine that fails to halt, or halts with a wrong output, on any well-formed input fails the definition. A proof must exhibit one fixed machine for all $n$.
• Infrastructure needed: Turing-machine composition with cost accounting; the Harvey–van der Hoeven reduction; the Nussbaumer synthetic transforms; the interchange and butterfly-layer networks of the preprint, with their rank and moment certificates; and the parameter assembly. The machine library and the certificate-checking infrastructure can be reused in other complexity missions.
• Welcome contributions: formal verification of the published certificates; formalization of the preprint's linear-network propositions; and machine-checked counterexamples to any step.

Selected references

• OpenAI, Integer multiplication below $n\log n$, preprint, 23 September 2026. https://github.com/openai/math/blob/main/preprints/Integer-multiplication-below-n-log-n-September-23-2026/paper.pdf
• D. Colkitt, A sharper exponent for integer multiplication (integer-mult-bounds), research draft, 2026. https://github.com/CrocSwap/integer-mult-bounds
• S. Jain, Integer multiplication: a conditional witness above $2^{-15}$ (integer-mult-kappa), research draft, 2026. https://github.com/Swapnil-jain/integer-mult-kappa
• D. Harvey, J. van der Hoeven, Integer multiplication in time $O(n\log n)$, Annals of Mathematics 193(2), 563–617, 2021. https://doi.org/10.4007/annals.2021.193.2.4
• A. Schönhage, V. Strassen, Schnelle Multiplikation großer Zahlen, Computing 7, 281–292, 1971. https://doi.org/10.1007/BF02242355
• H. J. Nussbaumer, Fast polynomial transform algorithms for digital convolution, IEEE Transactions on Acoustics, Speech, and Signal Processing 28(2), 205–215, 1980. https://doi.org/10.1109/TASSP.1980.1163372

Certify $\alpha\ge2.006470828$ by specializing OpenAI's general seed theorem to $d=20$ and $M=9^{21}$.

The construction gives

Here $bs(f,0)$ is block sensitivity at the all-zero input. The ratio $\log B/\log A$ is approximately $2.006470828227379\ldots$. Prove the exact inequality $A^{2.006470828}\le B$, then reuse the foundation's finite-certificate theorem.

The goal uses the campaign's shared definitions and requires arbitrarily large sensitivity. This is a stronger specialization of the existing construction, not a claim of a new construction or global parameter optimality.

Motivation

Nonlinear programming algorithms are routinely advertised as finding a local minimum. Most of them only certify first-order conditions (a KKT point), and the natural next question is whether a given feasible point is in fact a local minimum. For smooth problems where the Hessian is nonsingular this is a second-order test, but in the degenerate case the test itself becomes a combinatorial question about a quadratic form restricted to a cone.

K. G. Murty and S. N. Kabadi (Math. Programming 39 (1987) 117–129) showed that this question is intractable already in its simplest instance: deciding whether $x = 0$ is a local minimum of a quadratic form $x^{\mathsf T}Dx$ on the nonnegative orthant is NP-complete, and so is deciding whether a square integer matrix is copositive. The paper is the standard reference for the hardness of copositivity testing, which matters for copositive programming, for second-order optimality checks in constrained optimization, and for the complexity of local search in nonconvex optimization.

Setting

Let $D$ be a real square matrix of order $n$ and $Q(x) = x^{\mathsf T}Dx$. The matrix $D$ is copositive if $Q(x) \ge 0$ for every $x \ge 0$ (coordinatewise). The paper considers the quadratic program

and the following questions, each phrased so that "yes" is the interesting answer:

• Problem 1. Is $x = 0$ not a local minimum of (7)?
• Problem 2. Is $Q$ not bounded below on $\{x \ge 0\}$?
• Problem 3. Is there an $x \ge 0$ with $Q(x) < 0$ (is $D$ not copositive)?
• Problem 4. Given $a_0 > 0$, is there an $x \ge 0$ with $e^{\mathsf T}x = a_0$ and $Q(x) < 0$? Here $e$ is the all-ones vector.
• Problems 11, 12. With $h(u) = (u_1^2, \dots, u_n^2)\,D\,(u_1^2, \dots, u_n^2)^{\mathsf T}$, the objective of the unconstrained problem (15): is $u = 0$ not a local minimum of $h$ on $\mathbb R^n$, and is $h$ not bounded below?

The source problem is subset sum (Problem 5): given positive integers $d_0; d_1, \dots, d_n$, is there $y \in \{0,1\}^n$ with $\sum_j d_j y_j = d_0$? Let $l$ be the total number of digits in the data. The paper fixes an integer $\delta > 4\big(d_0\sum_j d_j\big)^2 n^3$ and a rational $\varepsilon$ with $0 < \varepsilon < 2^{-nl^2}$, and defines functions of $2n$ nonnegative variables $(y, s)$:

$f_2 = f_1 + 2d_0\sum_j d_j y_j(1 - y_j)$, a homogeneous quadratic $f_4$ that agrees with $f_2$ on the set

and $f_5 = f_4 - (\varepsilon/n^2)\big(\sum_j (y_j + s_j)\big)^2$. The function $f_5$ is a quadratic form $x^{\mathsf T}Mx$ in $x = (y, s) \in \mathbb R^{2n}$; the symmetric matrix $M$, with entries computed explicitly from $d_0, d, \delta, \varepsilon$, is the output of the reduction.

Formalization targets

Goal: the reduction is correct

For positive integer data $d_0; d_1, \dots, d_n$ and $\delta, \varepsilon$ as above, with $M$ the matrix of $f_5$, the following are equivalent:

This is the mathematical content of Theorems 1–3 and §4: a polynomially computable map from subset sum instances to matrices under which every one of these questions has the answer of the subset sum instance.

Milestones along the paper's chain

1. Problems 5 and 6 are equivalent: subset sum is solvable iff some $(y,s) \in P$ has $f_1 \le 0$.
2. Problems 6 and 7 are equivalent ($f_1$ vs. $f_2$ on $P$).
3. Problems 7 and 8 are equivalent ($f_2$ vs. $f_4$ on $P$).
4. Lemma 2: for an integer symmetric $D$ of size $L$, the minimum of $Q$ over $[0,1]^n$ is $0$ or at most $-2^{-L}$.
5. Problems 8 and 9 are equivalent: $\exists\,(y,s)\in P$ with $f_4 \le 0$ iff $\exists\,(y,s)\in P$ with $f_5 < 0$.
6. Problem 9 is a special case of Problem 4: $f_5(y,s) = x^{\mathsf T}Mx$, and Problem 9 is Problem 4 for $(M, a_0 = n)$.
7. Problems 3 and 4 are equivalent, for any $D$ and $a_0 > 0$.
8. Problems 1 and 2 are equivalent to Problem 3, for any $D$.
9. Problems 11 and 12 are equivalent to Problems 1 and 2, for any $D$.

Significance

The result. The equivalence shows that checking local optimality of a feasible point, checking boundedness of a quadratic objective on a cone, and checking copositivity are all at least as hard as subset sum, hence NP-hard. Through (15) the same holds for local minimality and boundedness of a quartic polynomial with no constraints at all. These facts are the standard justification for why nonconvex solvers settle for KKT points, and the copositivity part underlies the hardness of copositive programming.

The formalization. The paper's claims are proved, and have been cited for decades, but the proof as printed is a sketch: several steps are stated as "clearly" or "it can be verified", and one step of the proof of Theorem 1 (p. 125) is false as written. The inequality $(\delta/2)(y_j + s_j - 1)^2 + 2d_0 d_j y_j(1 - y_j) \ge 0$ for $y_j > 1$ fails for $y_j$ slightly above $1$, and the pointwise implication "$f_2 \le 0 \Rightarrow f_1 \le 0$ on $P$" has an explicit counterexample. The equivalence of Problems 6 and 7 itself survives numerical checks. A machine-checked proof of the goal settles the correctness of the reduction with the paper's own constants. No machine-checked proof of these statements exists on the platform.

Difficulty

The combinatorial direction (a subset sum solution gives a point with $f_5 < 0$) is a computation. The converse direction carries the content, in two places.

First, passing from $f_1$ to $f_2$ trades the linear penalty for a quadratic one. This is harmless on the box $0 \le y \le 1$ but not for $y_j > 1$, where $2d_0d_jy_j(1-y_j)$ is negative. The printed argument handles this coordinate by coordinate and is wrong there; a correct argument has to show that no point of $P$ with $f_2 \le 0$ exists unless a point with $f_1 \le 0$ does, which requires a global use of the size of $\delta$.

Second, passing from $f_4 \le 0$ to $f_5 < 0$ requires a quantitative gap: if $f_4 > 0$ on $P$ then $\min_P f_4 \ge \varepsilon$ with $\varepsilon$ of only polynomially many bits. Lemma 2 provides such a gap for the unit box and integer matrices, but $P$ is not the box and $f_4$ has rational coefficients, so the lemma does not apply verbatim.

The remaining equivalences (Problems 1, 2, 3, 4, 11, 12 for a fixed matrix) follow from homogeneity of the quadratic form and the substitution $x_j = u_j^2$, and are routine.

Formalization scope

The data $d_0, d_j, \delta$ are natural numbers and $\varepsilon$ is rational; all are cast to $\mathbb R$ in $f_1, \dots, f_5$ and $M$. The index $j = 1, \dots, n$ is Fin n, and the $2n$ variables of $M$ are indexed by Fin n ⊕ Fin n with $x =$ Sum.elim y s. Standing hypotheses: $d_j > 0$ and $d_0 > 0$ (the paper's "all positive integers"); $\delta > 4(d_0\sum_j d_j)^2n^3$ in $\mathbb N$; $\varepsilon > 0$ and $\varepsilon \cdot 2^{nl^2} < 1$ in $\mathbb Q$. The size $l$ counts decimal digits. Problem 1 is local minimality relative to the orthant, Problem 11 is unconstrained local minimality, both in the Euclidean topology. Lemma 2 is stated for integer symmetric $D$ (as §4 of the paper says, "as before … symmetric"), with $L$ Schrijver's encoding size, since the paper does not define "the size of $D$"; the "optimum is $0$ or $\le -2^{-L}$" is stated as a disjunction without an infimum. The milestones on $f_2, f_4, f_5$ over $P$ assume $n \ge 1$, which the paper assumes tacitly; the goal needs no such hypothesis.

Not formalized: membership in NP (Lemma 1), the polynomial-time computability of $M$ and its encoding size, the NP-completeness of subset sum (cited by the paper from Garey–Johnson), Theorem 4, and any of the words "NP-complete" or "NP-hard". The platform's complexity layer (Turing machines over bitstrings) has no subset sum problem and no encoding of rational matrices. The matrix $M$ has rational entries; a positive integer multiple of it is the integer matrix of Theorem 3, has the same answer to every question, and the rescaling is not formalized. The §3 standing assumption "D is not PSD" is not imposed; the constructed matrix can be PSD and the equivalence holds regardless.

The goal is about the explicit matrix $M$, whose entries are given in the definitions; it is not about "some matrix whose quadratic form is $f_5$", and the constants $\delta$ and $\varepsilon$ are the paper's explicit bounds, not "sufficiently large" or "for some $\varepsilon$". A formalization that quantifies existentially over the matrix or the precision would be trivially true and is ruled out.

Contributions welcome: proofs of the matrix identity and the homogeneity arguments (milestones 6–9), a proof of Lemma 2 (which needs a Cramer/Hadamard bound on basic solutions of the linear complementarity system (9)), and a correct proof of the $f_1 \leftrightarrow f_2$ step. The copositivity definitions and milestones 7–9 are reusable for any later work on copositive programming.

Selected references

• K. G. Murty and S. N. Kabadi, Some NP-complete problems in quadratic and nonlinear programming, Mathematical Programming 39 (1987) 117–129. https://doi.org/10.1007/BF02592948
• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979 (subset sum, problem [SP13]).
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986 (encoding sizes, §2.1).

Resource constraints and the easy/hard borderline in scheduling

Machine scheduling asks how to assign jobs to machines over time so that a criterion such as the makespan $C_{\max}$, the time at which the last job completes, is as small as possible. In practice jobs also compete for scarce resources beyond the machines themselves: tools, operators, memory, power. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the standard three-field classification $\alpha\mid\beta\mid\gamma$ of Graham, Lawler, Lenstra and Rinnooy Kan (1979) by a resource field $res\lambda\sigma\rho$. They then settled the complexity of every problem with parallel identical or uniform machines, unit-time jobs, precedence constraints and the $C_{\max}$ criterion. Their Fig. 2 separates the maximal polynomially solvable problems from the minimal NP-hard ones, and it has been the reference map for resource-constrained scheduling since.

Brief timeline of the problems involved:

• 1975. Garey and Johnson (SIAM J. Comput. 4) show that $P2\mid res\cdots, p_j=1\mid C_{\max}$ is solvable in polynomial time via matchings, and that $P3\mid res1\cdot\cdot, p_j=1\mid C_{\max}$ and $P2\mid res1\cdot\cdot, tree, p_j=1\mid C_{\max}$ are NP-hard in the strong sense, by reduction from 3-PARTITION.
• 1976. Ullman (Complexity of sequencing problems, in Coffman, ed., Computer & Job/Shop Scheduling Theory, Wiley) gives strong NP-hardness of $P2\mid res111, prec, p_j=1\mid C_{\max}$ under arbitrary precedence constraints.
• 1983. Błażewicz, Lenstra and Rinnooy Kan prove Theorem 7: chains suffice. Two identical machines, one resource of size one, requirements in $\{0,1\}$ and chain-like precedence already give a strongly NP-hard problem. The result dominates both earlier two-machine results.

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines $M_1,\dots,M_m$. Every job has processing time $1$ on every machine, each machine handles at most one job at a time, and jobs are not preempted. There are $l$ resources; resource $R_h$ has a positive integer size $s_h$, the amount available at any time, and job $J_j$ has a nonnegative integer requirement $r_{hj}$, the amount it holds throughout its execution. A directed acyclic graph $H$ on the jobs gives the precedence constraints: if $H$ has a path from $j$ to $k$ ($J_j\to J_k$), then $J_j$ must complete before $J_k$ starts. The precedence is chain-like when every vertex of $H$ has indegree and outdegree at most one.

A schedule gives each job a machine and a real start time $S_j$; the job occupies $[S_j, S_j+1)$ and completes at $C_j = S_j+1$. It is feasible if jobs on one machine do not overlap, precedence is respected, and at every time $t$ the jobs running at $t$ require at most $s_h$ of each resource $R_h$. The makespan is $C_{\max} = \max_j C_j$.

The problem $P2\mid res111, chain, p_j=1\mid C_{\max}$ restricts this to $m=2$, one resource ($\lambda=1$) of size $1$ ($\sigma=1$), every requirement at most $1$ ($\rho=1$), and chain-like precedence. The problem $P3\mid res1\cdot\cdot, p_j=1\mid C_{\max}$ has $m=3$, one resource of arbitrary size and requirements, and no precedence.

3-PARTITION: given $t$, a positive integer $b$ and positive integers $a_1,\dots,a_{3t}$ with $\sum_j a_j = tb$ and $\tfrac14 b<a_j<\tfrac12 b$, can $\{1,\dots,3t\}$ be split into $t$ disjoint 3-element sets $S_i$ with $\sum_{j\in S_i}a_j=b$?

A problem is NP-hard in the strong sense if it remains NP-hard when every number of the instance is written in unary.

Formalization targets

Goal: Theorem 7

The hypothesis is Garey and Johnson's theorem on 3-PARTITION, which the paper cites and does not prove. The conclusion concerns the decision version: given an instance and $y\in\mathbb N$, is there a feasible schedule with $C_{\max}\le y$?

Milestones

1. Proof of Theorem 4, the saturation equivalence. For positive $b$, $a_j$ with $\sum_j a_j=tb$, the $P3\mid res1\cdot\cdot$ instance with $3t$ unit jobs, resource size $b$ and requirements $a_j$ has a feasible schedule with $C_{\max}\le t$ iff the 3-PARTITION instance has a solution.
2. Theorem 4 (Garey and Johnson). Under the same hypothesis as the goal, $P3\mid res1\cdot\cdot, p_j=1\mid C_{\max}$ is NP-hard in the strong sense.
3. Proof of Theorem 7, "if". A 3-PARTITION solution yields a feasible schedule of the constructed two-machine instance with $C_{\max}=2tb$.
4. Proof of Theorem 7, "only if". A feasible schedule of the constructed instance with $C_{\max}\le 2tb$ yields a 3-PARTITION solution.

Significance

Theorem 7 is the sharpest hardness result of the paper's classification. Without resources, two-machine unit-time scheduling with arbitrary precedence is polynomial (Coffman and Graham, Acta Inform. 1972); without precedence, it is polynomial under arbitrary resources (Theorem 1 of the paper). The theorem shows that combining the weakest nontrivial versions of both constraints, chains and one unit resource, already crosses the borderline. The paper's §4.1 extends the same reduction to the $\sum C_j$ and $L_{\max}$ criteria.

On the formal side, the mission provides a machine-checked model of resource-constrained scheduling with real start times, a definition of NP-hardness in the strong sense on top of the platform's Turing-machine formalization of $\mathrm P$ and $\mathrm{NP}$, and 3-PARTITION as a reusable source problem. As far as the platform's corpus shows, none of Theorems 4 and 7, 3-PARTITION, or strong NP-hardness has been formalized before. Both theorems are proved in the literature; what remains is to formalize the reductions and their polynomial running time.

Difficulty

The combinatorial heart is the "only if" direction: a schedule of length $2tb$ must be shown to be rigid. Start times are arbitrary reals, so the first obstacle is to show that both machines are busy throughout $[0,2tb)$, that the chain $L$ forces unit spacing, and that the primed jobs of the chains $K'_j$ can only run in the intervals the chain $L$ leaves free of the resource. Only after this is established can the index sets $S_i$ be read off. Arguing on integer time slots from the start is not enough: the model allows fractional start times, and ruling them out is part of the proof.

The second obstacle is the complexity layer. NP-hardness is stated with respect to polynomial-time many-one reductions computed by one-tape Turing machines. The reduction from 3-PARTITION therefore has to be implemented and its running time bounded on unary codes. The constructed instance has $4tb$ jobs, which is polynomial in the unary length of the 3-PARTITION instance; this is exactly why the reduction proves hardness in the strong sense.

Formalization scope

• Model. Jobs are Fin n and machines Fin m, 0-based. Only identical machines with unit processing times are modelled. Start times are real, execution intervals are half-open, and the resource constraint is imposed at every real time. Precedence is the transitive closure of the arc list of $H$. $C_{\max}=0$ for an empty instance.
• Decision version. Thresholds $y$ are natural numbers; this narrower class makes the hardness statement stronger.
• Encoding. An instance is described by its list of numbers ($n,m,l$, the sizes, the requirements row by row, the number of arcs and the arcs, then $y$). The unary language is the set of unary codes of yes-instances over a two-letter alphabet. No pairing function is used. The class conditions (two machines, one unit resource, requirements at most one, chain-like acyclic $H$) are part of the yes-predicate.
• Strong sense. Strong NP-hardness is NP-hardness of the unary language. This is equivalent to Garey and Johnson's definition, which bounds the largest number by a polynomial in the instance length.
• Cited hypothesis. The goal and Theorem 4 assume strong NP-hardness of 3-PARTITION (with $\tfrac14 b<a_j<\tfrac12 b$) and nothing else. Stating the goal as a bare reduction between the two languages, or adding $\mathrm P\ne\mathrm{NP}$, would not be Theorem 7.
• Constructions. The two scheduling instances built from a 3-PARTITION instance are explicit definitions following the page, not arbitrary instances with a property.
• Reuse. The scheduling model and the strong-NP-hardness layer are shared with the other missions of this series; 3-PARTITION serves any strong NP-hardness proof by number partitioning.

Welcome contributions: proofs of the four milestones; a formalized polynomial-time implementation of the reduction on unary codes; general lemmas about composing polynomial-time reductions on the one-tape machine model.

Selected references

• J. Błażewicz, J. K. Lenstra, A. H. G. Rinnooy Kan, Scheduling subject to resource constraints: classification and complexity, Discrete Applied Mathematics 5 (1983) 11–24. https://doi.org/10.1016/0166-218X(83)90012-4
• M. R. Garey, D. S. Johnson, Complexity results for multiprocessor scheduling under resource constraints, SIAM J. Comput. 4 (1975) 397–411. https://doi.org/10.1137/0204035
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, 1979.
• R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Ann. Discrete Math. 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• J. D. Ullman, Complexity of sequencing problems, in: E. G. Coffman, Jr., ed., Computer & Job/Shop Scheduling Theory, Wiley, 1976, 139–164.
• E. G. Coffman, Jr., R. L. Graham, Optimal scheduling for two-processor systems, Acta Informatica 1 (1972) 200–213. https://doi.org/10.1007/BF00288685
• S. Cook, The P versus NP problem, Clay Mathematics Institute official problem description.

Prove a separation exponent of 2.127294, building on Robin Kothari’s 2.075 construction and yousofy’s 2.105 proof with twelve nested predicates and sharper joint boundary bounds.

Motivation

Multiplying two $n$-bit integers on a multitape Turing machine takes $O(n\log n)$ steps by the algorithm of Harvey and van der Hoeven (2021), and $n\log n$ was long conjectured to be optimal. The OpenAI manuscript Integer multiplication below $n\log n$ (September 2026) gives a machine running in time $O(n\,L(n)^{1-\kappa})$ with $\kappa = 2^{-182}$, which beats $n\log n$ by a factor that grows without bound. That theorem is now fully formalized on this platform: IntMul.Kappa.campaign_bound_inv_two_pow_182 is Proved, through the published development NLogN.KFTop.kappa_bound.

The manuscript calls its constants "deliberately conservative; no optimization is claimed." The community repository CrocSwap/integer-mult-bounds records which constants the same construction tolerates. Its patch frozen-154 keeps the original swap networks and recurrence exponents and changes only four constants of the final assembly, which raises the saving to $\kappa = 2^{-154}$. This mission formalizes that retuning.

Timeline of the saving $\kappa$ for this construction:

• 2026, OpenAI manuscript: $\kappa = 2^{-182}$, with $\varepsilon = 2^{-75}$, $c = 2^{-56}$, $\lambda' = 1 - 2^{-54}$, $\tau = 1 - 2^{-50}$. Formalized on Prove2me in October 2026.
• 2026, frozen-154 patch: $\kappa = 2^{-154}$, with $\varepsilon = c = 2^{-51}$, $\lambda = 1 - 2^{-101}$, $\lambda' = 1 - 2^{-102}$, and the same networks. Not yet formalized.
• Later community rounds (new networks, Jain's rounds six to eight) reach $\kappa \approx 10^{-4}$. They are separate entries in this campaign, and their machine-level theorems are still Open.

Setting

A multitape Turing machine has a finite alphabet, finitely many states, a read-only input tape, an output tape and finitely many work tapes. On input $x\#y$ with $x, y \in \{0,1\}^n$ it must halt with the $2n$-bit binary expansion of $\mathrm{val}(x)\cdot\mathrm{val}(y)$ on the output tape. Write $L(n) = \max(\lceil \log_2 n\rceil, 1)$. The proposition $\mathrm{KappaBound}(\kappa)$ (from IntMul_MultitapeModel) says that one such machine is correct for every $n \ge 1$ and runs in at most $C\,n\,L(n)^{1-\kappa}$ steps for all large $n$.

The OpenAI machine processes inputs of length $n$ using the parameters $b = L(n)$, $p = 6b$, $d = \lfloor b^{\varepsilon}\rfloor$ (the number of axes of the transform), $K = \lfloor d^{c}\rfloor$ (the chunk width of the transform layout), $\ell = \lceil L/d\rceil$ and $\alpha = \lceil (12 d^2 b)^{1/4}\rceil$, where $L$ is least with $4n \le 2^L b$ and $V = 2^L p$ is the bit volume. Its running time divided by $V$ is bounded by the normalized cost table (Table 1 of the manuscript)

Each row is at most $p$ to a power below one. The seven margins below one are

and the saving is $\kappa = \tfrac12\min_i g_i$. At the manuscript's constants the minimum is $g_2 = 2^{-181}$. At the frozen-154 constants ($\tau = 1-2^{-50}$ and $\delta = 1/16$ unchanged) the minimum is $g_3 = 2^{-153}$, so $\kappa = 2^{-154}$.

The definition file IntMul_OpenAI_R154 fixes these constants, the table $N$ (named Ncost) and the parameter map dP, KP, ℓP, αP. It reuses $b$, $L$, $T$, $p$ and $V$ from the published IntMul.OpenAI.Glue, since they do not depend on the constants.

Formalization targets

Goal

This is the campaign template with value $1/2^{154}$, stated over the campaign's foundation definitions.

Milestones

1. Margins: at the new constants, $2\kappa \le g_i$ for all seven margins, together with the layer conditions $\tau(1 + c/\beta) < \lambda' < 1$ (with $\beta = 1/2$) and $\lambda' - \tau - c > 0$.
2. Cost table: under the pointwise bounds $p^{\varepsilon}/12 \le d \le p^{\varepsilon}$, $p^{\varepsilon c}/24 \le K \le p^{\varepsilon c}$, $0 \le \ell \le p/(3d)$, $0 \le \alpha \le 4p^{1/4+\varepsilon/2}$, one has $N(p,d,K,\ell,\alpha) \le 50\,p^{1-2\kappa}$.
3. Parameters: for all large $n$, the concrete parameters satisfy those pointwise bounds with $p = 6L(n)$, and $0 \le V \le 48n$.
4. Reduction: a correct machine whose time is at most $C_0\big(V\cdot N \cdot (\log L(n) + 1)^A + n\big)$ for all large $n$, with any parameter sequences obeying the pointwise bounds, satisfies $\mathrm{KappaBound}(2^{-154})$.
5. Machine: there is a correct multitape machine whose time is at most $C_0\big(V\cdot N(6L(n), d, K, \ell, \alpha)\cdot(\log L(n)+1)^A + n\big)$ for all large $n$, at the concrete frozen-154 parameters.

The goal follows from milestones 3, 4 and 5 by a short argument.

Significance

The result itself. The bound improves the formally verified saving for exact integer multiplication on multitape machines from $2^{-182}$ to $2^{-154}$, a factor of $2^{28}$, without new mathematics in the networks. It also checks that the manuscript's construction is robust to its constants, which the manuscript asserts but does not exercise.

Formalizing it. The $2^{-182}$ development hard-codes $\varepsilon$ and $c$ in its parameter map (IntMul.OpenAI.Glue.dP, KP) and in the statements built on them. A development written against general constants, or a second instantiation, makes every later retuning cheap and separates what depends on the constants from what does not. Milestones 1 to 4 are short and mirror proved lemmas of the $2^{-182}$ development. Milestone 5 is the substance.

Difficulty

The cost analysis is not where the difficulty lies; it is finite arithmetic with real powers. The difficulty is milestone 5: re-establishing the machine's time bound at the new $d$ and $K$. A larger $\varepsilon$ makes $d$ grow much faster with $b$, and a larger $c$ makes the chunk width $K$ grow faster with $d$. Every lemma whose proof used the old exponents numerically must be rechecked. These include the depth guard for the recursive layers, the bound on the simultaneous-layer exponent $\lambda'$, and the requirement that the auxiliary gate counts fit in $p + 3$ bits. Reusing the $2^{-182}$ proofs verbatim fails wherever they rely on $d \le b^{2^{-75}}$ or $K \le d^{2^{-56}}$ specifically.

Formalization scope

All statements use the Mathlib environment of the campaign (0df444a, Lean v4.33.1) and the machine model IntMul_MultitapeModel: a fixed finite alphabet and state set, $k \ge 2$ one-way infinite tapes, a read-only input tape, and exact output $\mathrm{bin}_{2n}(\mathrm{val}(x)\mathrm{val}(y))$. Real powers are Real.rpow. $L(n) = \max(\lceil\log_2 n\rceil, 1)$ is IntMul.lg.