EpsilonEridani
Let’s formalize lots of physics.
AI-authored Lean formalizations of the physics of the Electron-Ion Collider — from scattering kinematics to QCD — directed by human-owned roadmaps and gated by open, adversarial review.
Humans own the roadmap
Physicists set the targets — nucleon spin, hadron mass, gluon saturation, 3D imaging — in a separate, human-reviewed roadmap repository. People choose the physics.
AIs write the code
AI agents formalize kinematics, symmetries and the relations between observables in Lean and open pull requests — every statement machine-checked, no sorries, no stray axioms.
Open review gates everything
AI reviewers judge each PR against fixed, open-source rubrics — correctness, reuse, API, naming, generality — and hunt for mis-formalized physics before it can merge.
On the roadmap
SpinStructure
Spin structure of the proton and neutron
HadronMassAndEnergyMomentumTensor
The hadron mass, the energy-momentum tensor, and gravitational form factors
SmallXAndSaturation
Small-x evolution, gluon saturation, and the Color Glass Condensate
GeneralizedPartonDistributions
Generalized parton distributions and spatial imaging
Growing fast
See the statistics →Three repositories
A taste of the physics
One-loop asymptotic freedom, the SU(3) adjoint Casimir, and DVCS momentum transfer — each example is checked against the library when this page is built.
open EpsilonEridani.QFT.QCD in
/-- Asymptotic freedom — the one-loop coefficient of the QCD β-function is
β₀ = 11 − (2/3) n_f, so QCD is asymptotically free for fewer than 16.5 quark flavours. -/
theorem asymptotic_freedom (nF : ℝ) (h : 2 * nF < 33) :
beta0 (suNColorFactors 3 nF) = 11 - (2 / 3) * nF ∧
IsAsymptoticallyFree (suNColorFactors 3 nF) :=
⟨nF:ℝh:2 * nF < 33⊢ beta0 (suNColorFactors 3 nF) = 11 - 2 / 3 * nF nF:ℝh:2 * nF < 33⊢ 11 / 3 * 3 - 2 / 3 * nF = 11 - 2 / 3 * nF; All goals completed! 🐙, isAsymptoticallyFree_qcd nF h⟩open EpsilonEridani.QFT.QCD.RepresentationColor in
/-- The adjoint Casimir of SU(3) — the Gell-Mann structure constants satisfy
Σ_{c,d} f^{acd} f^{bcd} = 3 δ^{ab}, i.e. C_A = 3, checked over every index. -/
theorem su3_adjoint_casimir (a b : Fin 8) :
(∑ c : Fin 8, ∑ d : Fin 8, structConst3 a c d * structConst3 b c d) =
3 * su3DeltaAdj a b :=
su3AdjointStatement a bopen EpsilonEridani.QFT.Scattering.DIS.Exclusive.Kinematics in
/-- Momentum transfer in deeply virtual Compton scattering — momentum conservation
p + q = p' + q' makes the hadronic t = (p' − p)² equal to the photon-side (q − q')². -/
theorem dvcs_momentum_transfer {V : Type} [AddCommGroup V] [Module ℝ V]
(g : LinearMap.BilinForm ℝ V) (K : ExclKinematics V) :
K.tMom g = g (K.q - K.qPrime) (K.q - K.qPrime) :=
K.tMom_eq_photon_transfer_sq gBuilt on Tau Ceti
EpsilonEridani is built on Tau Ceti, the open-source project whose AI-driven formalization and review machinery it extends from mathematics to phenomenological physics.