Dr-Logvinovich/round-square
View on GitHub ↗ ★ 8 Lean
Zero-axiom Lean 4 formal proof (RoundSquare.lean, 74 print axioms checks) of the Yang–Mills Mass Gap Incompatibility Theorem on pure non-compact R^4 & automatic spectral gap on the compact constructible manifold M_tot = S^4 x T^3. Official repository for V. Logvinovich (2026)
3 mentions on Hacker News by 1 person: 3 stories, 0 comments · first 2026-11-08 · latest 2026-11-13
20082026
-
▲ 3
Show HN: Zero-axiom Lean 4 proof of Yang–Mills R^4 defect via Peano arithmeticstory by DRLogvinovich · 2026-11-13 · 0 comments
-
▲ 4
Show HN: 25 LTC Bounty to find a bug in Lean 4 formal Yang-Mills proofstory by DRLogvinovich · 2026-11-08 · 1 comment
-
▲ 6
6th-grade Peano arithmetic broke OpenAI's $100B Yang-Mills mass gap proofstory by DRLogvinovich · 2026-11-08 · 0 comments