Joshua Wharton · QFEX · joshua@qfex.com
The complete Lean project proves
for the challenge's exact deterministic integer APSP problem. Its closed theorem Race.bound provides a correct finite word-RAM program and a proof of its actual execution time, including the required input, output, memory, and word-width conditions. It has no unproved numerical, oracle, correctness, or execution-cost hypotheses.
This refines the 2.99556085 exponent listed as Lean Verified on Big O Speedrun on 20 October 2026. The decrease is exactly 0.000000084. It retunes the executable parameters of Li Xuanji's complete proof, following Hrishik Sai Bojnal's earlier numerical refinement. Original algorithm, compiler, and proof attribution is preserved.
Run the complete verification with:
cd verified
lake exe cache get
python3 verify.pyThe verification builds the sources, checks that the challenge statement is unchanged, checks the exact rational theorem type, and audits all transitive axioms of that theorem. The successful verification transcript and checked source hashes record the local result. The independent candidate CI run also passed both proof jobs. See provenance and changed files and the full build instructions.
This complete theorem is for 2.995560766. The faster exponent 2.9929479187094, described below, remains conditional on unformalized machine implementation obligations. The complete proof above does not establish that faster exponent. Local proof checking does not mean the challenge has reviewed or accepted this new result.
The machine/ directory contains two newly checked components toward the faster construction: a selected-row controller and all twelve local row encoders. Their execution, memory, and resource proofs are complete at the component level. The encoder refinement also proves equality to the imported upstream row definition and an execution-time comparison with its scalar counter. The remaining full-program obligations are stated explicitly.
An exact numerical certificate for the conditional deterministic integer APSP bound
This refines the exponent 2.99294792 displayed as Claimed on the Big O Speedrun APSP challenge when examined on 20 October 2026. The decrease in the exponent is exactly 0.0000000012906.
Read the research note (PDF), its LaTeX source, the complete word-RAM proof, or the faster bound’s numerical Lean proof.
The accompanying Lean development proves 47 strict numerical inequalities and all exact stage identities, with the entropy expressions defined using Mathlib's actual Real.log. It also proves a common reserve of 2 × 10⁻¹⁴ in the inequalities, controls all stages of both phases, and derives the stated exponent for the explicit mathematical cost ledger, including fixed logarithmic factors and upward rounding. The independent Python checker verifies the same numerical conditions using rational interval arithmetic. These conditions come from the aligned Walsh embedding, polynomial query cache, and composite-incidence construction in the pinned upstream note.
The APSP bound is conditional on that construction's written algorithmic proof and word-RAM cost interpretation. The theorems in lean/ establish the numerical certificate and the mathematical cost ledger. A complete challenge EndStatement.APSP theorem at 2.9929479187094, including a correct machine program and a proof of its execution cost, remains unproved. The fixed stage count is enormous and the certified slack is very small; no global optimality or practical speedup is claimed.
The contribution here is a refined rational parameter witness, its Lean formalization, an independently implemented exact checker, a reproducible numerical search, and an explanatory note. The underlying algorithm and adapted proof architecture are attributed to the sources below and in the Lean file headers. The materials were prepared with AI assistance; the separate reviews mentioned in the note were AI-agent reviews. This repository records the refinement and is not a submission to, or verification by, the challenge.
The project pins Lean 4.33.1 and an exact Mathlib commit. Follow the setup instructions, then run:
cd lean
lake build
lake env lean Audit.leanThe main results are ApspBound.Analytic.analyticNumericalCertificate and ApspBound.Ledger.refinedExponentBigO. The audit rejects any transitive axiom beyond propext, Classical.choice, and Quot.sound; the development uses no admitted proofs or native decision axioms. The Lean README states the exact theorem and the remaining machine-program obligations. Citation metadata records the author, affiliation, and contact.
Use Python 3.10 or later. No third-party Python packages are required. From this directory, run:
python3 verify_certificate.py --json certificate.jsonThe final output should include:
PASS: 47 strict rational inequalities and all exact stage identities.
Certified exponent: 2.9929479187094
Smallest certified runtime gap: 0.0000000000000224020591996589
This certifies numerical feasibility, not the full word-RAM theorem.
The script reads the exact decimal strings in parameters.json. All verification arithmetic uses Python's Fraction. Logarithms are enclosed by a 40-term positive series with an explicit rational remainder bound; decimal output is rounded outward and does not decide whether a condition passes. Explicit exceptions keep the checks active under python3 -O as well.
certificate.json contains the machine-readable results, including all lower and upper bounds. verification.txt records the successful console output.
Treat each decimal below as an exact rational number.
| Parameter | Exact value |
|---|---|
c |
10.665500244065729 |
theta |
0.06529782369872631 |
b |
0.046046352103722105 |
R |
1000000000000 |
S |
768979037380 |
Target saving delta |
0.0070520812906 |
Exponent 3 - delta |
2.9929479187094 |
The stage variables are defined exactly by eta = b/R, u = S*eta, v = (R-S)*eta, and e = b+u. The note derives the cost expressions and explains why checking the endpoints covers both phases of the construction.
python3 optimize_parameters.pyThis optional search uses Python Decimal with 80-digit working precision. It locates a stationary point of the balanced limiting objective, guiding the choice of the rational witness. It does not prove a global optimum, and the exact checker does not depend on its output. The recorded search output is in optimization.txt.
With pdfLaTeX and the packages listed in the LaTeX source installed:
pdflatex -interaction=nonstopmode -halt-on-error apsp_refinement.tex
pdflatex -interaction=nonstopmode -halt-on-error apsp_refinement.texThe second pass resolves internal references. The resulting PDF is apsp_refinement.pdf.
Three upstream finite checkers were also rerun during preparation. These provide finite corroboration of parts of the inherited construction; they do not prove its asymptotic correctness and are separate from the exact parameter certificate in this repository.
| Upstream checker | Observed result |
|---|---|
| Aligned embedding | 352 original matrix outputs checked |
| Aligned cache | 34 arbitrary signed-array queries and 20 encoders checked |
| Aligned integration | 530 normalized scalar and cyclic coefficients checked |
To reproduce those checks, use the full upstream checkout so its supporting modules are available:
git clone https://github.com/shreshth-s/thin-matrix-results.git
cd thin-matrix-results
git checkout --detach 8a21eaae81599913dba562727e03a9b48c36a5b9
python3 outputs/check_five_term_aligned_embedding.py
python3 outputs/check_five_term_aligned_cache.py
python3 outputs/check_five_term_aligned_integration.pyThe direct algorithmic source is GitHub author shreshth-s, Improving the displayed exponents in arXiv:2610.06783v1, in thin-matrix-results/outputs/exponent-improvement.tex, pinned to commit 8a21eaae81599913dba562727e03a9b48c36a5b9. Relevant dependencies include the aligned Walsh embedding and polynomial-cache lemmas and equations (A1)–(A13).
The construction builds on:
- Josh Alman and Virginia Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs, 2026.
- Ruhollah Majdoddin, Thin matrix products up to D ≤ N^0.172 and lossless reductions for 3SUM, Exact Triangle and APSP, with 3SUM over abelian groups and a dichotomy for coordinatewise problems, 2026.
The research note identifies the inherited proof dependencies and the limits of the refinement in more detail.