Generating novel, thermodynamically stable inorganic crystals

LeMat-GenBench (Dec 2025) evaluated 12 recent crystal generative models on a unified metric set and found that increases in stability come at the cost of novelty and diversity on average, with no model excelling across all dimensions - i.e. as of Sep 2026 the field has no generator that is simultaneously stable, novel, diverse and synthesisable.

Source: arxiv.org

No prize money is attached to this problem.

import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.Finset.Card
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum

/-!
# Generating novel, thermodynamically stable inorganic crystals

Concrete here: **energy above the convex hull**. For a chemical system with `n`
elements, a phase diagram is a finite set of reference entries, each a
composition (atom fractions over the `n` elements) with a formation energy per
atom. The hull energy at a composition is the minimum energy attainable by any
convex mixture of reference entries having that composition, so
"energy above hull ≤ ε" is exactly: *every* composition-matching mixture has
energy at least `candidate.energy - ε`. That is the lower convex envelope,
written as a universally quantified inequality — no oracle is needed for it.

Opaque oracle (`Verification`): the formation energies themselves (DFT
relaxation at a fixed, declared functional and convergence settings), whether a
generated structure is *novel* against a declared snapshot of known materials,
and whether two generated structures are duplicates under a declared structure
matcher. Also oracle: that the generator's weights were frozen before the
reference snapshot was fixed.

Who must attest: the benchmark host (e.g. a Matbench-Discovery- or
LeMat-GenBench-style evaluator) publishing the reference snapshot hash, the DFT
settings, the matcher tolerances, and the relaxed energies for every submitted
structure.

Units: energies in eV per atom; compositions are dimensionless atom fractions
summing to 1. The conventional stability window is 0.03 eV/atom above hull;
0 eV/atom means on the hull.

Checked with Lean 4.33.0 / Mathlib using:
  lake env lean <absolute-path-to-this-file>
-/

namespace OpenSpur.Problems.StableCrystalGeneration

/-- Atom fractions over `n` elements. -/
abbrev Comp (n : ℕ) := Fin n → ℝ

/-- A composition with its formation energy per atom (eV/atom). -/
structure Entry (n : ℕ) where
  comp : Comp n
  energy : ℝ

/-- The competing-phase set of a chemical system, indexed by `Fin size`. -/
structure PhaseDiagram (n : ℕ) where
  size : ℕ
  entry : Fin size → Entry n

/-- `w` is a convex mixture of reference phases with the same composition as `c`. -/
def IsMixtureOf {n : ℕ} (D : PhaseDiagram n) (c : Entry n)
    (w : Fin D.size → ℝ) : Prop :=
  (∀ i, 0 ≤ w i) ∧
  (∑ i, w i) = 1 ∧
  (∀ j, (∑ i, w i * (D.entry i).comp j) = c.comp j)

/-- Energy per atom of a mixture (eV/atom). -/
def mixtureEnergy {n : ℕ} (D : PhaseDiagram n) (w : Fin D.size → ℝ) : ℝ :=
  ∑ i, w i * (D.entry i).energy

/-- Concrete: the candidate lies at most `ε` eV/atom above the lower convex
envelope of the reference phases. -/
def AboveHullAtMost {n : ℕ} (D : PhaseDiagram n) (c : Entry n) (ε : ℝ) : Prop :=
  ∀ w, IsMixtureOf D c w → c.energy - ε ≤ mixtureEnergy D w

/-- Per-structure facts only measurement or a matcher can supply. -/
structure Verification (n : ℕ) where
  /-- DFT-relaxed entry (composition + energy per atom) used for the hull test. -/
  relaxed : Entry n
  /-- Absent from the declared snapshot of known materials. -/
  novel : Prop
  /-- Not a duplicate of any earlier accepted submission under the matcher. -/
  unique : Prop

/-- Stability window and yield demanded of a submission. -/
structure Thresholds where
  /-- Hull window in eV/atom, e.g. 0.03. -/
  hullWindow : ℝ
  /-- Minimum count of stable-unique-novel structures required. -/
  minSUN : ℕ

/-- The conventional stability window, eV/atom. -/
def defaultHullWindow : ℝ := 0.03

/-- One submitted structure clears the bar. -/
def SUN {n : ℕ} (D : PhaseDiagram n) (T : Thresholds) (v : Verification n) : Prop :=
  v.novel ∧ v.unique ∧ AboveHullAtMost D v.relaxed T.hullWindow

/-- A submission: finitely many structures, each with its verification record,
plus the attestation that generation preceded the reference snapshot. -/
structure Submission (n : ℕ) where
  count : ℕ
  verification : Fin count → Verification n
  frozenBeforeSnapshot : Prop

/-- Acceptance: at least `minSUN` submitted structures are stable, unique and
novel. `accepted` names them; the predicate forces each one to clear the bar. -/
def Solved {n : ℕ} (D : PhaseDiagram n) (T : Thresholds) (S : Submission n)
    (accepted : Finset (Fin S.count)) : Prop :=
  S.frozenBeforeSnapshot ∧
  T.minSUN ≤ accepted.card ∧
  ∀ i ∈ accepted, SUN D T (S.verification i)

/-- Rung `k` keeps the 0.03 eV/atom window and demands `100 * (k+1)` SUN hits. -/
def Rung (k : ℕ) : Thresholds where
  hullWindow := defaultHullWindow
  minSUN := 100 * (k + 1)

/-- Widening the hull window can only preserve the hull test. -/
theorem aboveHull_mono {n : ℕ} (D : PhaseDiagram n) (c : Entry n) {ε₁ ε₂ : ℝ}
    (h : ε₁ ≤ ε₂) : AboveHullAtMost D c ε₁ → AboveHullAtMost D c ε₂ := by
  intro hc w hw
  have := hc w hw
  linarith

/-- Solving a higher rung implies solving every lower rung. -/
theorem solved_rung_mono {n : ℕ} (D : PhaseDiagram n) {j k : ℕ} (h : j ≤ k)
    (S : Submission n) (accepted : Finset (Fin S.count)) :
    Solved D (Rung k) S accepted → Solved D (Rung j) S accepted := by
  intro hs
  obtain ⟨hfrozen, hcard, hsun⟩ := hs
  refine ⟨hfrozen, ?_, hsun⟩
  have : 100 * (j + 1) ≤ 100 * (k + 1) := by
    have : j + 1 ≤ k + 1 := Nat.succ_le_succ h
    exact Nat.mul_le_mul_left 100 this
  exact le_trans this hcard

end OpenSpur.Problems.StableCrystalGeneration

• LeMat-GenBench leaderboard (Hugging Face Space)
• LeMat-GenBench evaluation suite (code)
• LeMat-Bulk dataset (~6.7M rows, harmonised MP/OQMD/Alexandria)
• Matbench Discovery leaderboard (crystal stability, geometry, phonons)
• MatterGen (Microsoft, MIT-licensed model + training data)
• GNoME predictions (380k stable structures contributed to Materials Project)