Lean

Formalisation projects in Lean.

• Finite algebras of length at most sixteen are smoothable: formal proof
  A complete formal proof in Lean 4 that, over an algebraically closed field of characteristic zero, every finite quotient of k[x,y,z] of length at most 16 is smoothable, with no added axiom. It formalises the main theorem of Fourteen points in three-space and lengths 15 and 16 of Nineteen points in three-space.
  Lean source (tar.gz, 843 KB)Details
• Normality of smooth lattice three-polytopes: formal proof
  A complete formal proof in Lean 4 that every smooth three-dimensional lattice polytope is normal. It formalises the article on the AI results page.
  Lean source (tar.gz, 166 KB)Article (PDF)Details

Finite algebras of length at most sixteen

The theorem

The main theorem, in Hilb3/Main/B16.lean, and the axioms it depends on:

theorem Hilb3.hilb_le_sixteen {k : Type*} [Field k] [IsAlgClosed k] [CharZero k]
    (I : Ideal (MvPolynomial (Fin 3) k)) [Module.Finite k (MvPolynomial (Fin 3) k ⧸ I)]
    (hI : Module.finrank k (MvPolynomial (Fin 3) k ⧸ I) ≤ 16) :
    Smoothable k (MvPolynomial (Fin 3) k ⧸ I)

#print axioms Hilb3.hilb_le_sixteen
-- 'Hilb3.hilb_le_sixteen' depends on axioms: [propext, Classical.choice, Quot.sound]

In words: over an algebraically closed field of characteristic zero, every quotient of k[x,y,z] of finite length at most sixteen is smoothable. The same statement over ℂ is Hilb3.hilb_le_sixteen_complex; Hilb3.hilb_le_fifteen, hilb_le_fourteen, hilb_le_thirteen and hilb_le_twelve are the cases of length at most 15, 14, 13 and 12. The proof uses only the three standard axioms of Lean’s logic: no sorry, no added axiom and no native_decide.

Results from the literature. The articles use several published results as black boxes. The formalisation proves the ones it needs, with the statements given in Hilb3/Axioms.lean: the linkage theorem of Jelisiejew, Ramkumar and Sammartano (arXiv:2409.17009, Section 5.1). With S = k[x,y,z] and m = (x,y,z): if m^N ⊆ (f,g,h) + m^N+1 and J = (f,g,h) + m^N ⊆ I, then the lengths of S/(J:I) and S/I add up to that of S/J, and S/I is smoothable if and only if S/(J:I) is. It also proves Gotzmann’s persistence theorem and Macaulay’s bound in the cases used, the length abc of a complete intersection of three forms without common zero, and the smoothability of very compressed algebras (Douvropoulos, Jelisiejew, Nødland and Teitler). The file also declares one axiom, the smoothability of finite Gorenstein subschemes (Buchsbaum–Eisenbud, Kleppe), which is used only by an alternative argument for one case kept in the source; no main theorem depends on it, as the axiom list above shows and the archive’s VERIFY.sh checks.

What “smoothable” means

A basis of a d-dimensional algebra gives its structure constants, a point of k^d×d×d. The étale locus is the set of structure constants of the split algebra k^d in all of its bases, and an algebra is Smoothable when its structure constants, in some basis, lie in the Zariski closure of the étale locus. These definitions, verbatim from the source:

/-- The Zariski closure of `S ⊆ σ → k`: common zeros of all polynomials vanishing on `S`. -/
def zclosure (S : Set (σ → k)) : Set (σ → k) :=
  {x | ∀ p : MvPolynomial σ k, (∀ y ∈ S, eval y p = 0) → eval x p = 0}

/-- The structure constants of `A` in the basis `b`: `b i * b j = ∑ l, structConst b (i, j, l) • b l`. -/
noncomputable def structConst {A : Type*} [CommRing A] [Algebra k A] {d : ℕ}
    (b : Basis (Fin d) k A) : SCIdx d → k :=
  fun ijl => b.repr (b ijl.1 * b ijl.2.1) ijl.2.2

/-- The étale locus: structure constants of the split algebra `Fin d → k` in all of its bases. -/
def etaleLocus (d : ℕ) : Set (SCIdx d → k) :=
  Set.range fun b : Basis (Fin d) k (Fin d → k) => structConst b

/-- A (finite) commutative `k`-algebra is smoothable if, in some basis, its structure constants lie in
the Zariski closure of the étale locus. An algebra without a finite basis is not smoothable. -/
def Smoothable (A : Type*) [CommRing A] [Algebra k A] : Prop :=
  ∃ (d : ℕ) (b : Basis (Fin d) k A), structConst b ∈ zclosure (etaleLocus k d)

That this agrees with smoothability in the Hilbert scheme of points of affine three-space — so that the theorem says that the Hilbert scheme of d points in 𝔸³ is irreducible for d ≤ 16 — is a published result (Cartwright, Erman, Velasco and Viray, Hilbert schemes of 8 points, Lemma 4.1). It is cited, not formalised.

Checks

• Clean build of the published archive with Lean 4.34.0 and Mathlib db00fb39: no errors and no sorry; the archive’s VERIFY.sh passes.
• Lean’s kernel re-checked every declaration, including all of Mathlib (leanchecker --fresh).
• The independent type checker nanoda re-checked the main theorems and the 77 099 declarations they depend on, permitting only the three standard axioms.
• The statements were written a second time using only Mathlib and the definition above (check/ in the archive) and proved from the theorems of the project.
• For lengths at most twelve, two independent reviews of the formal statements against the article found no error.

Building it

tar xzf points_in_three_space_lean.tar.gz
cd points_in_three_space_lean
lake exe cache get     # downloads prebuilt Mathlib
lake build
./VERIFY.sh            # hashes, clean rebuild, sorry scan, axioms, statement check

This needs elan. SHA-256 of the archive: 0ce2e289db0b9984f406047771003619a33c38bfb7011774f299a2b80fa76d6f
Licence: PolyForm Strict 1.0.0. Free to download, build and use for noncommercial purposes; no changes, redistribution or sale.

About this formalisation

The formalisation was produced by AI agents working from the articles Fourteen points in three-space and Nineteen points in three-space, which it follows in outline but not always in detail: 230 files and about 76 000 lines. It contains Zheng’s theorem on finite quotients of surfaces with a rational double point in the cases the proof needs (types A_n, D_n and E₆), with a proof of its own; the cases of type E₇ and E₈ that occur are obtained as limits of type E₆.

For the very compressed algebras the formalisation proves that k[x,y,z]/I is smoothable whenever (x,y,z)⁴ ⊆ I ⊆ (x,y,z)³, in every length from 10 to 20 (Hilb3.smoothable_veryCompressed_three), by an elementary form of the strategy of Douvropoulos, Jelisiejew, Nødland and Teitler: limits of scaled configurations of points, a Jacobian criterion for density, and an exact rational certificate for each case, checked by Lean’s kernel. The linkage theorem is proved directly for the notion of smoothability above, by deforming a complete intersection over a smoothing of the residual scheme; one ingredient is that a factor of a smoothable product of algebras is smoothable.

Status. Lengths up to sixteen: complete, standard axioms only. Lengths seventeen to nineteen, treated in Nineteen points in three-space: in progress.

Previous versions remain available: lengths at most fifteen, assuming the linkage theorem, points_in_three_space_lean_v3.tar.gz (SHA-256 787053fff616b3d26d2eedbac7ed0b9a64281677e41f7daa52cb3e2f453a40be); lengths at most fourteen, points_in_three_space_lean_v2.tar.gz (SHA-256 fc6ec6de6fa871b91d27009bc3090d205df68c08d8b2c3dce6676c1958b465cd); lengths at most twelve, points_in_three_space_lean_v1.tar.gz (SHA-256 c3dc79fce73646c6dbd812067bb0a4fd7998649967e25fd0eb6f4e40abe8352d).

Normality of smooth lattice three-polytopes

The theorem

The main theorem, in Odanorm/Main.lean, and the axioms it depends on:

theorem oda_normality_dim_three (P : SmoothPolytope) : IsNormal P.carrier

#print axioms Odanorm.Main.oda_normality_dim_three
-- 'Odanorm.Main.oda_normality_dim_three' depends on axioms: [propext, Classical.choice, Quot.sound]

These are the three standard axioms of Lean’s logic. The proof uses no sorry, no added axiom and no native_decide, and lake build itself checks the axiom list.

What the statement says

Normality is the integer decomposition property: for every k ≥ 1, every lattice point of kP is a sum of k lattice points of P. A SmoothPolytope is a lattice polytope in ℝ³ given both by an irredundant facet description with primitive normals and by its vertices; at every vertex it coincides locally with the cone spanned by a basis of ℤ³. The source also proves that the unit cube is a SmoothPolytope, so the theorem is not vacuous.

Below is everything the statement refers to apart from Mathlib, verbatim from the source (pr is declared under variable {n : ℕ}).

/-- The ambient real space. -/
abbrev E (n : ℕ) := Fin n → ℝ

/-- The lattice `M ≅ ℤⁿ`. -/
abbrev L (n : ℕ) := Fin n → ℤ

/-- The inclusion `M ↪ M_ℝ`. -/
def toE {n : ℕ} (x : L n) : E n := fun i => (x i : ℝ)

/-- A lattice covector, viewed in `M_ℝ` via the standard identification `N ≅ ℤⁿ`. -/
def covectorToE {n : ℕ} (b : L n) : E n := fun i => (b i : ℝ)

/-- The `k`-fold dilate.  For convex `S` this agrees with the `k`-fold Minkowski sum. -/
def dilate {n : ℕ} (k : ℝ) (S : Set (E n)) : Set (E n) := {x | ∃ s ∈ S, x = k • s}

/-- `P` is `k`-normal: every lattice point of `kP` is a sum of `k` lattice points of `P`. -/
def KNormal {n : ℕ} (P : Set (E n)) (k : ℕ) : Prop :=
  ∀ z : L n, toE z ∈ dilate (k : ℝ) P →
    ∃ f : Fin k → L n, (∀ i, toE (f i) ∈ P) ∧ z = ∑ i, f i

/-- `P` is normal (has the integer decomposition property). -/
def IsNormal {n : ℕ} (P : Set (E n)) : Prop := ∀ k : ℕ, 1 ≤ k → KNormal P k

/-- The pairing `⟪u, y⟫` used throughout. -/
def pr (u y : E n) : ℝ := ∑ i, u i * y i

/-- `e` is a `ℤ`-basis of `M = ℤ³`. -/
def IsLatticeBasis (e : Fin 3 → L 3) : Prop :=
  ∀ x : L 3, ∃! t : Fin 3 → ℤ, x = ∑ j, t j • e j

/-- `u ∈ N` is primitive: nonzero, and not a proper multiple of a lattice covector. -/
def IsPrimitive (u : L 3) : Prop :=
  u ≠ 0 ∧ ∀ (k : ℤ) (v : L 3), u = k • v → k = 1 ∨ k = -1

/-- **A smooth lattice three-polytope**, `thm:main`.

Fields `hfacets`/`hverts` carry the two descriptions of the same set; Minkowski–Weyl,
which would produce one from the other, is not available, so both are data.  `hprim`,
`hinj`, `hirred` say the normals are *primitive*, *pairwise distinct*, and that the
presentation is *irredundant*, which is what `\eqref{eq:facet-presentation}` gives; mere
attainment of each inequality would be weaker, and is derived from `hirred` as
`FacetDepthCore.attained`.  `hfulldim` is
`dim P = 3`. `hextreme` says `verts` really is the vertex set (no point of it is in the
hull of the others).  `hsmooth` is smoothness. -/
structure SmoothPolytope where
  /-- the index set of the facets -/
  ι : Type
  fintypeι : Fintype ι
  nonemptyι : Nonempty ι
  /-- the primitive outward facet normals `u_ρ ∈ N` -/
  u : ι → L 3
  /-- the right-hand sides `a_ρ` -/
  a : ι → ℝ
  /-- the vertex set -/
  verts : Finset (L 3)
  /-- the polytope `P ⊆ M_ℝ` -/
  carrier : Set (E 3)
  /-- `P = {x : ⟪u_ρ, x⟫ ≤ a_ρ for every ρ}` -/
  hfacets : carrier = {x : E 3 | ∀ j, pr (covectorToE (u j)) x ≤ a j}
  /-- `P = conv(verts)`, so `P` is a lattice polytope -/
  hverts : carrier = convexHull ℝ (toE '' (verts : Set (L 3)))
  /-- the normals are primitive -/
  hprim : ∀ j, IsPrimitive (u j)
  /-- distinct facets have distinct normals -/
  hinj : Function.Injective u
  /-- **the presentation is irredundant** — `\eqref{eq:facet-presentation}`.  No
  inequality may be dropped: for every `j` the body cut out by the *other* inequalities
  differs from `P`.  (It always *contains* `P`, so `≠` is strict containment, i.e. some
  point satisfies every inequality but the `j`-th.)  This is what makes the `u j` the
  facet normals; mere *attainment* of each inequality would be strictly weaker, and is
  recovered from this field as the theorem `FacetDepthCore.attained` below. -/
  hirred : ∀ j, carrier ≠ {x : E 3 | ∀ l, l ≠ j → pr (covectorToE (u l)) x ≤ a l}
  /-- `dim P = 3` -/
  hfulldim : affineSpan ℝ (toE '' (verts : Set (L 3))) = ⊤
  /-- `verts` is exactly the vertex set -/
  hextreme : ∀ v ∈ verts, toE v ∉ convexHull ℝ (toE '' ((verts : Set (L 3)) \ {v}))
  /-- **smoothness**: at every vertex `P` is locally the simplicial cone spanned by a
  lattice basis -/
  hsmooth : ∀ v ∈ verts, ∃ (e : Fin 3 → L 3) (ε : ℝ), 0 < ε ∧ IsLatticeBasis e ∧
      ∀ x : E 3, dist x (toE v) < ε →
        (x ∈ carrier ↔ ∃ t : Fin 3 → ℝ, (∀ j, 0 ≤ t j) ∧ x = toE v + ∑ j, t j • toE (e j))

Checks

Carried out on the archive on 26 September 2026. On 28 September only the licence was added; the code is unchanged and the new archive passes VERIFY.sh again.

• Clean build from the archive with Lean 4.34.0 and Mathlib db00fb39: no errors and no sorry.
• Lean’s kernel re-checked every declaration, including all of Mathlib (leanchecker --fresh).
• The independent type checker nanoda re-checked the theorem and everything it depends on (39 201 declarations, including the parts of Mathlib it uses), permitting only the three axioms above.

Building it

tar xzf oda_normality_lean.tar.gz
cd oda_normality_lean
lake exe cache get     # downloads prebuilt Mathlib
lake build
./VERIFY.sh            # hashes, clean rebuild, sorry scan, axioms

This needs elan; the archive pins the Lean toolchain and the Mathlib commit. SHA-256 of the archive: 449dc2f91d01be395a08a11605561d483a551d49e93000ca7079753b9267c2e2

Licence: PolyForm Strict 1.0.0 (file LICENSE in both archives). Free to download, build and use for noncommercial purposes; no changes, redistribution or sale.

About this version

This is a shortened version of the original formal development: 46 files and about 10 700 lines instead of 71 files and 37 000, with the same theorem and the same definitions. Several steps are proved differently from the article; for instance, a single “octahedron lemma” replaces the route through Howe’s theorem and Pick’s formula in Section 7 and the odd-index argument in Section 8, and the matrix lemma is used in a scaled form that needs no invertibility. The README.md in the archive lists the changes. An earlier, longer version (about 21 000 lines) remains available: tar.gz. The opening section of the article describes how the proof and the formalisation were produced.