Swapnil Jain: OpenAI problem #109 past 2^-15, certificates and assembly checked in Lean
Swapnil Jain @SJ_Swapnil_JainX
Why it matters
Sixth update (~102k views), reaching 2^-15 about 90 minutes before Colkitt’s community repo and claiming Lean kernel checks.
Summary
Posted 14:03 UTC on 8 Oct. The Lean files (core Lean 4, decide) check histogram rank sums, moment bounds and the κ assembly inequalities; per the README, analytic premises, the upstream theorem and independent review are not covered.
Archived text
Sixth update to OpenAI problem #109 (integer multiplication): we are now past 2^-15.
κ > 2⁻¹⁵ (tightened from κ = 2⁻¹⁸²)
The exact witness is 3.667 × 10⁻⁵, about 2.4 fold over our previous 1.548 × 10⁻⁵, and a 2¹⁶⁷ fold improvement over the original OAI result.
Both interchange certificates and the full assembly are checked in Lean’s kernel.
Quoting @SJ_Swapnil_Jain: Fifth update to OpenAI problem #109 (integer multiplication): we are now past 2^-16.