A multi-agent AI framework formalizing the Yang-Mills Mass Gap finite-lattice theory in Lean 4 without axioms or sorry.
-
Updated
Oct 31, 2026 - Lean
A multi-agent AI framework formalizing the Yang-Mills Mass Gap finite-lattice theory in Lean 4 without axioms or sorry.
The mass gap over the compact simple groups
Deriving the Standard Model from a single finite geometry with zero free parameters
OPEN PROBLEMS WANT TO STAY OPEN
Lean 4 scaffold for formalizing the Yang–Mills existence and mass gap problem, with checked finite-dimensional certificates and a staged continuum-lift program.
Machine-verified foundations for quantum field theory in Lean 4 (ACMD) — 3,323 kernel-checked theorem declarations. Every claim tiered; kills published next to the proofs.
Unified Information-Density Theory v3.9 - Vacuum Information Density as the Fundamental Geometric Scalar: A Proposed Theoretical Framework for the Yang-Mills Mass Gap and Gamma-Scaling Unification
A rigorous Lean 4 formalization aiming to computationally verify the unconditional proof of the Yang-Mills mass gap (a Clay Millennium Prize Problem).
This paper investigates the ”double field theory” (DFT) and the connection to the double copy method that shows that gauge & gravity theories are remarkably similar at the quantum level.
AI-generated solutions to two research-level math problems from the First Proof community experiment: a Yang-Mills gauge-fixing heat-flow estimate on the 2-torus, and sharp fatness of geodesic triangles in sparse random graphs. Produced autonomously in Claude Code, offered for human validation.
Structural proofs of eight millennium-type problems / 八道千禧年型问题的结构证明:统一结构层(1 / 笛卡尔积 / 位值幂 b^k、基底 729=3^6、四则运算 ≅ Klein 四元群)+ 谱结构方法(层内谱 Z_2^k、层间嵌套、闭合条件 nm=k、生成律 A(N)、闭包律 Q(N)、递推 x^6-49x^4+504x^2-1296)
Machine-checked Lean 4 proofs: Wilson's area law for SU(N) lattice gauge theory, and the Fisher-Lorentz identities. Axiom gate in the build, zero sorry.
The central research hub for the VYTYLS Initiative. Hosting the Field of Consciousness (FoC) Lattice Gauge Theory, the Reality Fold Notation (RFN) and Modal Layer Tiers (MLT) methodology, and the Cybernetic Acoustic Research of the VYTYLS duo.
Research record for 'Retained Geometry and Certified Gauge Cutoffs': the Sept 8 paper and scripts, Sept 9 spatial SU(3) calculations, and Lean 4 checks of specified finite algebra. No continuum mass gap is claimed.
Reproducible proofs for P vs NP, Yang-Mills Mass Gap, and Riemann Hypothesis using parameter-free Jabri Identity Zₜ=1. Zero fitted parameters. Python code, data, and Zenodo DOI included. Author: Abdulla Al-Jabri.
Rust lattice-gauge simulation engine (MILL): validated 2D U(1) baseline plus active 4D SU(3) pure-gauge kernel with Cabibbo-Marinari heatbath/overrelaxation and mass-effective diagnostics.
Candidate Lean 4 statement of the Yang–Mills existence and mass gap problem, with compiled guards against fake models (not a proof)
Six independent formal proofs for the Yang-Mills Existence and Mass Gap problem, covering RG Flow, Analytic Continuation, and Heat Kernel methods.
Generated physics: Yang-Mills mass gap, three fermion generations, mass relations, gauge couplings and cosmology. V5 has 261 derived records and 57 benchmark comparisons; 51/56 central-value rows are within 1% of adopted references. Reproducible spectral calculations from minimal change.
To associate your repository with the yang-mills topic, visit your repo's landing page and select "manage topics."