Release
This page identifies the exact files behind the paper’s computer-assisted claims: the PDF, the Lean formalisation, the code and data of the computer-assisted proofs, and the record of the Lean build.
Status: Not yet frozen. The files on this site are those of the manuscript of 2 November 2026. No release has been tagged or archived yet; when the paper is submitted, its revision will be frozen as release v1, tagged, and archived on Zenodo with a DOI.
Identity
| Paper | Path Decompositions of Sparse Graphs via Gaussian Sweeps and Faster Exponential Algorithms, manuscript of 2 November 2026 |
| Research repository commit | 17040c5 (serggasp/treewidth-cubic) |
| Release | none yet |
| Archived copy | 10.5281/zenodo.23883489 (reserved) |
Files
| File | Contents |
|---|---|
sparse-pathwidth.pdf |
the paper |
lean/ |
the Lean 4 project (Mathlib), with lean-toolchain, lakefile.toml and lake-manifest.json |
ancillary/ |
the code and data of the computer-assisted proofs; SHA256SUMS lists their checksums |
evidence/build-info.txt |
the record of the Lean build on Serge’s MacBook Pro |
evidence/axioms.txt |
the axioms of the Lean theorems, printed by that build |
Lean
The Lean project was built from scratch on Serge’s MacBook Pro (Apple silicon, 16 cores), with lake build of both libraries and #print axioms of the final theorems; the formalisation page gives the details and the commands to repeat the check. The site’s own build renders the pages and checks their links; it never builds Lean.
Computer-assisted proofs
ancillary/README.md says what each folder computes and how to run it. The driver experiments/reproducibility/run_all.sh reproduces the certificate of the width bounds for maximum degree \(4\) and \(5\) and of the charging certificate of the median-switched sweep: its quick mode (about one minute) rechecks the stored data in exact arithmetic; its full mode (about 80 minutes on 16 cores) recomputes them in ball arithmetic.