Lean formalizes a sharp product-free set theorem from Gowers and collaborators
satnam6502 · x · 2026-07-25
Pietro Monticone says Aristotle helped formalize a preprint by W. T. Gowers and collaborators, and that the long case analysis is now formally verified in Lean.
- The proof concerns a sharp result: if \(A\) is an open product-free subset of \((0,1)\), then its measure is less than \(1/3\).
- The author notes the referee-unfriendly case analysis has been checked formally in @LeanProver.
- The code should appear on GitHub soon.
- After more cleanup, parts of the supporting API may be upstreamed into Mathlib.
More from Research
- Paper: AI Text Is Hard to Read Because LLMs Optimize for Density, Not Communication — rickasaurus · 2026-10-26
- Does LeWorldModel Preserve Local Action Geometry? Gram Matrix Analysis Says Barely — Vasil Vasilev · 2026-10-26
- Busy Beaver explainer video hits 100k views in one day — Paimaamu · 2026-10-26
- Toggling a Single Neuron Turns Qwen into Cookie Monster—Plus a Zoo Map — burny_tech · 2026-10-26
- A neural net learns 2^100 LDPC codewords from just 10-20 examples — DimaKrotov · 2026-10-26
- AGMAI advises AI labs against designating mathematicians to vet model math outputs — AlexKontorovich · 2026-10-26