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.
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.
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.
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…
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.
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.
To associate your repository with the computer-assisted-proofs topic, visit your repo's landing page and select "manage topics."