A software that assists a previous version of the proof of Gerver's conjecture, using a custom geometric branch-and-bound algorithm, and the exact rational QP solver powered by CGAL
Library for computer-assisted proofs in dynamical systems
Autonomous mathematical research by Qiushi Engine: a structural tensor-rank lower bound of 21 for 3x3 matrix multiplication over F2, with complete Lean formalization, bilingual reports, and an open research trajectory.
Not a Clay solution. Spectral-front identities for periodic Navier-Stokes: a bandwidth-dissipation dichotomy, an exact action representation, and an obstruction to uniform pointwise Osgood closure. Exact-rational certificates; AI-agent review, not human peer review.
Primes p ≤ N with N − p an almost prime sum of two squares (Ω ≤ 9): paper, semi-linear vector sieve with Richert weights and switching, and an interval-arithmetic certification script.
Reproducible computer-assisted proof candidate for Erdos Problem 23, with exact rational certificates and a verifier. Unrefereed.
N = n₁ + n₂ with n₁, n₂ sums of two squares (or values of any class number one form) and Ω(n₁n₂) ≤ 11, max Ω(nᵢ) ≤ 8: paper, linear vector sieve with switching and Richert weights, interval-arithmetic certification.
A particle is bouncing on a vertically vibrating parabolic surface. For a given number of impacts between the particle and the surface, periodic orbits are provided for fixed parameter values. A folder containing the code capable of finding these orbits as well as doing rigorous pseudo-arclength continuation in the surface's amplitude of oscilla…
Proposed bound for Erdos Problem 36 with directed-rounding verification and explicit upstream dependencies. Preliminary and unrefereed.
Proof artifacts and reproduction code for exact adaptivity thresholds in priced equality queries under complete equivalence promises.
Proofs and reproducible certificates for geometric conditions that yield zero optimized single-use coherent information but positive quantum capacity in flagged qubit channels with noisy measurement records, including a certified eight-use witness.
Partial bounds for Erdos Problem 302, with exact certificates and Lean verification materials. Preliminary and unrefereed.
To associate your repository with the computer-assisted-proofs topic, visit your repo's landing page and select "manage topics."