Pinned Loading

1. thomson-n7-log thomson-n7-log Public

   AI-produced, unreviewed Lean 4 warrant: the pentagonal bipyramid as the unique logarithmic-energy (and Riesz s = 2) minimiser for 7 points on the sphere (Conjecture 1 of Armentano et al.); also a s…

   Lean 2

2. covering-numbers covering-numbers Public

   AI-produced computational certificates for the covering numbers C(17,8,3), C(20,10,3), C(22,11,3) and the family C(2m,m,3) (not peer reviewed)

   Python

3. ramsey-cells ramsey-cells Public

   Computation records for small graph Ramsey cells: formulas, cube decompositions, verdict ledgers, and reconstruction scripts. Unconfirmed, not peer reviewed.

   Lean

4. smale-mean-value-degree6 smale-mean-value-degree6 Public

   AI-produced computational certificates (branch-and-bound, independent arb check, local certificates) for Smale's mean value conjecture in degree 6; not peer reviewed

   C

5. five-points-riesz five-points-riesz Public

   Exact three-point SDP certificates: the triangular bipyramid uniquely minimises the Coulomb (Thomson) and Riesz s=2 energies of 5 points on S^2 (known theorems, Schwartz). AI-produced warrant; not …

   Lean

6. kissing-number-4 kissing-number-4 Public

   AI-produced Lean 4 formalisation of the kissing number in dimension 4 with an exact three-point certificate (unreviewed, not peer reviewed)

   Lean