computer-assisted-proof

Research notes, exact computations, and reproducible verification for MathOverflow 413935

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.

Computer-assisted proofs and clean-room audits for the r=10 and r=11 fixed cases of Erdős Problem 617.

Exact verification code and certificates for phase transitions in generalized Damascus inequality violation sets.

Proofs, finite certificates, and reproducible SAT/XOR records for crossing-maximal complete-graph drawings.

Computer-assisted research on the covering number C(16,5,3). New certified lower bound: no 61-block cover exists, so 62 <= C(16,5,3) <= 65 (DRAT proofs verified). CC BY 4.0.

Proof claims and reproducible verification for the r=5,6,7,8 cases of Erdős Problem 617.

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

Counterexample family for finite grand couplings with reproducible computer-assisted state minimality

AI-assisted, unreviewed research artifact for a candidate 67.302666% lower bound on simple critical-line zeta zeros.

Certified optima vs the published search for the qubit-peeling factorisation of 'Wave packets from the spectrum' (arXiv:2606.10004): note, code and data.

Certified theorems closing the transitive case of Frankl's union-closed conjecture up to 15 points: no family invariant under any transitive permutation group on up to 15 points violates the conjecture. LRAT certificates, formally verified checking (cake_lpr). Sequel to frankl-cyclic-sat.

Improved irrationality-exponent bounds for log 3 and log₂ 3

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

Certified scoped theorem for binary covering sequences: every valid length-70 (9,1) cover uses at most 60 distinct edges in common with one fixed backbone; global bounds unchanged.

Computer-assisted proof that the 7₂ knot regulator integral in Ramanujan Challenge 3.1 equals 4π²/85.

Bernstein's constant to ten rigorously certified digits: beta = 0.2801694990, proved in interval arithmetic (Arb) where the 1985 Varga-Carpenter rigorous enclosure gives five. OEIS A073001. Every number re-derivable from the shipped data in exact arithmetic.

Certified eliminations in the planar six-body central-configuration problem: paper, certificates, pinned solver inputs, and a dependency-free reproduction pipeline

Arb-certified local descent near regular projective-response levels in quantum control.

Certificate-backed research on finite-sample conservatism of the Stringer audit bound