Lean 4 formalization of Erdős Problem #848 – seeking review (github.com) 1 points by vibecodermcswag 5mo ago ↗ HN
[–] vibecodermcswag 5mo ago ↗ Formalized the Sawhney-Sellke stability theorem for Erdős Problem #848 (squarefree products) in Lean 4.~3800 lines, compiles with 0 errors, no sorries, no axioms.The math was solved by Sawhney & Sellke (Nov 2025): https://arxiv.org/abs/2511.16072Only ~17 Erdős problems have full solutions formalized in Lean. If valid, this would be ~#18.Done with multiple AI tools (Claude Opus 4.5, GPT-5.2, Gemini 3.0, Aristotle) + human orchestration.Seeking review: Does this actually prove what it claims? The code is verbose and could be cleaner. Would appreciate expert eyes.
1 comment
[ 3.3 ms ] story [ 10.6 ms ] thread~3800 lines, compiles with 0 errors, no sorries, no axioms.
The math was solved by Sawhney & Sellke (Nov 2025): https://arxiv.org/abs/2511.16072
Only ~17 Erdős problems have full solutions formalized in Lean. If valid, this would be ~#18.
Done with multiple AI tools (Claude Opus 4.5, GPT-5.2, Gemini 3.0, Aristotle) + human orchestration.
Seeking review: Does this actually prove what it claims? The code is verbose and could be cleaner. Would appreciate expert eyes.