computer-assisted-proof

Minimum edges of a graph of treewidth k: cliques are optimal for k ≤ 7, then 34, 42, 47 and 53 for k = 8–11.

Computer-assisted two-sided proof of the logarithmic law of the resolution gap of the arrow of time on periodic windows, from strips to combs.

Deterministic bounded-normal minimax computation with an independent interval certificate.

Audit the declarations a computational result carries, and check they are still true. Producer freshness, counter coherence, provenance pins, partial runs. Read-only by construction.

Dimers on the square lattice and the king's graph: the entropy per site of king's graph dimers (s = 0.5655119110413253 ± 6e-16, with rigorous bounds) and exact domino (OEIS A004003) and domicule (A239273) counts to 20×20, with papers, data and notebooks.

Unrefereed candidate: computer-assisted proof that the square maximises λ₂/λ₁ (Dirichlet Laplacian) among all quadrilaterals, convex or not. Paper, certificates, verifiers, replay receipts. DOI 10.5281/zenodo.23109314

Computer-assisted (Arb) proof that the localized Weil quadratic form has a simple, even ground state for all L in (0, 1.09]. Code, certificate data, paper.

Explicit 4,096-cylinder cover of the regular tetrahedron with normalized area 0.4996138 (saving 3.86e-4 below 1/2), openai/math problem 100, with two independent exact checkers

Certificate, proof and two independent Arb checkers for C82 < 0.2534449 (essential minimum of the Zhang-Zagier height, Tao's optimization-constants table 82a)

Exact step-function certificates for Tao's constants C_1c and C_1d

An extremal even unimodular lattice in dimension 112 (minimum norm 10): paper draft, defining matrices, verification code and data, and a Lean 4 formalization of the deduction.

Exact copying limits of quantum states: Sidon phase codebooks, designs, stabilizer states (code + certificates for Papers 1–3)

Exact symmetric and two-sided Sidon-set certificates, with independently checked coefficient sqrt(ab) < 0.942809153974 and reproducible rational verification.

Computer-assisted proof that the univalent Bloch-Landau constant is below 0.65628589: slit domain, certificate programs and paper

(Erdős–Lovász cover number problem)A computer-assisted determination of g(6) = 17, the smallest pairwise intersecting 6-uniform family with transversal number 6. Four papers, and an explicit 17-card witness. Research draft: not independently reviewed, no priority claimed.

正十七边形 12 E 尺规作图研究 | Regular 17-gon construction: verified 12 E upper bound, exact replay, and Manim animation.

Draft (unpublished): exact explicit-formula verification of the function-field Legendre conjecture for d <= 10, fluctuations of prime counts, and a characteristic-2 anomaly.

Ten exact covering numbers C(v,k,3), e.g. C(18,11,3)=10, with machine-checked SAT proofs and a one-command reproduction

Packings of equal circles, spheres and hyperspheres (Packomania, 21 tables). 6,071 records released; 4,063 still best-known on 2026-10-18 (2,008 since beaten or tied by others, listed in SUPERSEDED.csv). Each verified by two independent exact checkers. By Moki&Julio.

Erdős Problem #616: t(21) = 4. Computer-assisted proof with an end-to-end Lean 4 formalization and verified SAT certificates (DRAT/LRAT).