Originally published on giftheory.substack.com

Toward machine-verified existence of G2 manifolds

Dec 10, 2025

"Does K7 actually exist?"

It’s a reasonable question. GIFT claims physics emerges from a 7-manifold with G2 holonomy. But claiming a manifold exists and proving it exists are different exercises.

In 1996, Dominic Joyce proved that compact G2 manifolds exist. The proof uses hard analysis: Sobolev spaces, implicit function theorems, contraction mappings. It spans some 200 pages of differential geometry.

We’ve now formalized key parts of that argument in Lean 4. Here’s what that means, and what it doesn’t. The challenge with existence theorems

Existence proofs in geometry are notoriously difficult to verify. They typically involve:

Infinite-dimensional function spaces
Estimates that "follow from standard elliptic theory"
Constants that are "sufficiently small"
Iterations that "converge by Banach’s theorem"

Each step may be correct. But the chain is long, and checking it requires expertise that’s not widely shared. The result: existence theorems get cited, but rarely re-derived from scratch.

Formal verification offers a different approach. What if a machine tracked every estimate? What Joyce’s theorem says

Let M be a compact 7-manifold with a G2 structure φ0. The structure has torsion T(φ0), measuring how far φ0 is from being "torsion-free": the desirable case, which implies Ricci-flatness.

Joyce’s Theorem (roughly): If ‖T(φ0)‖ < ε0 for some threshold ε0, then there exists a smooth torsion-free G2 structure φ on M, with ‖φ - φ0‖ ≤ C·‖T(φ0)‖.

In other words: if you find an approximate G2 structure with small enough torsion, an exact one exists nearby.

The subtlety: ε0 depends on Sobolev constants of M. Computing it for a specific manifold requires careful analysis. What the Lean formalization covers

The formalization has three layers:

Layer 1: Abstract framework

Sobolev spaces, differential forms, and the implicit function theorem are set up as Lean structures:

-- Sobolev embedding: H^4 continuously embeds in C^0 theorem sobolev_embedding_H4_C0 (M : Manifold) [Compact M] : ContinuousEmbedding (H 4 M) (C 0 M)

-- Hodge Laplacian is self-adjoint theorem hodge_laplacian_self_adjoint : IsSelfAdjoint (hodge_laplacian : Ω^k M → Ω^k M)

Layer 2: Joyce iteration as contraction

Joyce’s proof works by iterating a correction map. The formalization captures the key property: this map is a contraction with constant K < 1.

noncomputable def joyce_K : NNReal := ⟨9/10, by norm_num⟩

theorem joyce_K_lt_one : joyce_K < 1 := by simp [joyce_K]; norm_num

theorem joyce_is_contraction : ContractingWith joyce_K JoyceFlow := ⟨joyce_K_lt_one, joyce_lipschitz⟩

Layer 3: Banach fixed point

Mathlib provides the Banach fixed point theorem, proven from first principles in the library:

-- Existence via Mathlib’s ContractingWith.fixedPoint noncomputable def torsion_free_structure : G2Structures := joyce_is_contraction.fixedPoint JoyceFlow

theorem k7_admits_torsion_free_g2 : ∃ φ : G2Structures, IsTorsionFree φ := ⟨torsion_free_structure, fixed_point_is_torsion_free⟩

When this compiles, Lean has verified the logical chain from contraction to existence. The numerical side

Abstract existence needs grounding. We also need to check that K7 specifically satisfies Joyce’s hypotheses.

A physics-informed neural network (PINN) constructs an approximate G2 structure φ0 on K7. The network has roughly 200,000 parameters and trains in 5-10 minutes on free platforms like Colab.

The torsion bound is the critical one. Our estimate for Joyce’s threshold on K7 is ε0 ≈ 0.0288. The PINN achieves ‖T‖ = 0.00140.

Safety margin: approximately ×ばつ

This margin provides some confidence that the bound isn’t marginal. Of course, the true ε0 for K7 depends on Sobolev constants we haven’t computed exactly, more on that below. Axiom audit

What does the proof assume? Lean makes this explicit:

#print axioms k7_admits_torsion_free_g2

Standard axioms (from Lean/Mathlib):

propext: Propositional extensionality
Quot.sound: Quotient soundness

These are standard foundations, nothing exotic.

Domain axioms (interface to geometry):

K7 → K7 exists as a topological type → Abstract interface JoyceFlow → The iteration map exists → Joyce’s construction joyce_lipschitzJoyceFlow → has Lipschitz constant < 1 → Contraction property fixed_point_torsion_zero → Fixed points are torsion-free → Joyce’s theorem conclusion

Notably, the Banach fixed point theorem is not axiomatized: it comes from Mathlib’s ContractingWith.fixedPoint, proven within the library. What this does NOT prove

It’s worth being clear about the limitations:

Joyce’s theorem is not formalized from first principles. The analytical core, Sobolev estimates, elliptic regularity, Schauder theory, is axiomatized rather than proven in Lean. A complete formalization would be a substantial project, likely requiring years of work.
The threshold ε0 is estimated, not computed exactly. We use a conservative estimate based on typical Sobolev constants. The true value for K7 would require more detailed analysis.
The physics interpretation remains conjectural. The claim that our universe involves K7 compactification is empirical, not mathematical. This formalization doesn’t touch that question.
Uniqueness is unknown. Other G2 structures with these invariants may exist. The moduli space structure hasn’t been characterized.

What this does achieve

Despite the caveats, the formalization accomplishes something useful:

Machine-verified arithmetic. The bounds (×ばつ safety margin, det(g) match, etc.) are checked by Lean, not by hand.
Transparent assumptions. Every axiom is listed explicitly. There’s no hidden "trust me" step.
Reproducibility. Anyone can verify the computation:

pip install giftpy python -c "from gift_core.analysis import JoyceCertificate; print(JoyceCertificate.verify())"

Modular structure. The argument is broken into standalone lemmas. Each piece can be examined or improved independently.

The remaining work

The formalization connects two endpoints:

Top: Abstract existence via Banach fixed point (formalized)
Bottom: Numerical bounds from PINN training (certified)

The middle layer: Joyce’s analytical machinery, is currently axiomatized. Completing the picture would mean formalizing:

Elliptic regularity on compact manifolds
Sobolev multiplication and embedding theorems
Schauder estimates for nonlinear PDE

This is substantial mathematics. Similar efforts (like formalizing parts of Fermat’s Last Theorem) have taken years. We’re not claiming to have done it.

But the scaffolding exists. The theorem statement compiles. The numerical bounds are verified. What remains is filling in the analytical middle, a task that’s well-defined, if demanding. Conclusion

theorem k7_admits_torsion_free_g2 : ∃ φ : G2Structures, IsTorsionFree φ

This statement compiles in Lean 4.14.0 with Mathlib. Subject to the axioms listed above, the existence of a torsion-free G2 structure on K7 is machine-verified.

The axioms are explicit. The gaps are acknowledged. The numerical evidence is reproducible.

Whether this connects to physics is a separate question, one that experiments, not proof assistants, will eventually answer.

Repository: github.com/gift-framework/core

Notebook: github.com/gift-framework/GIFT/notebooks