Problem
Clean hydrogen at $1/kg (electrolysis at scale)
Clean hydrogen made by splitting water with renewable or low-carbon electricity could decarbonize ammonia, steel, refining and e-fuels, but it only displaces fossil (grey) hydrogen, typically about $1-2/kg, if its full production cost falls to roughly the same level. Electrolyzer makers compete on stack efficiency (kWh/kg), capital cost ($/kW), durability and operation on variable power, since electricity and capex dominate the levelized cost. The US DOE Hydrogen Shot defines the target: $1 per kg of clean hydrogen within a decade of 2021 (by 2031), with an interim $2/kg by 2026 and electrolyzer system cost of $250-500/kW. SOLVED means an unsubsidized levelized cost of hydrogen <= $1/kg at plant gate from commercial-scale (100 MW+) electrolysis with lifecycle emissions under the clean-hydrogen threshold, demonstrated with audited operating data.
Funding
Raised by the 3 companies working on it, 2 undisclosed.
Why it is still open
The IEA Global Hydrogen Review 2025 reports that low-emissions hydrogen stays costlier than unabated fossil production in the near term, the cost gap widened as gas prices fell and electrolyzer costs rose with inflation and slow deployment, and announced 2030 low-emissions production fell from 49 to 37 Mtpa, with electrolysis projects responsible for more than 80% of the drop. DOE's own baseline at Hydrogen Shot launch was about $5/kg for electrolytic hydrogen, and EU Hydrogen Bank winners still need subsidies of up to ~EUR 3.49/kg on top of market prices (2026 auction).
Source: iea.org
Who is working on it
Prizes
| Prize | Status | Pays for | Amount |
|---|---|---|---|
| European Hydrogen Bank auction 1 (Innovation Fund pilot) | Awarded | Ranking | — |
| European Hydrogen Bank auction 2 | Awarded | Ranking | — |
| European Hydrogen Bank auction 3 (IF25) | Awarded | Ranking | — |
| US Regional Clean Hydrogen Hubs (H2Hubs) | Closed, unawarded | Ranking | $7.00B |
What counts as solved
import Mathlib /-! # Clean hydrogen at $1/kg (electrolysis at scale) Target modelled on the US DOE Hydrogen Shot ("1 1 1": $1 per 1 kg in 1 decade) with the DOE Clean Hydrogen Production Standard (lifecycle ≤ 4.0 kg CO2e / kg H2, well-to-gate). A board may substitute EU RFNBO (≤ 3.38 kg CO2e / kg H2). Concrete in Lean: the levelized cost of hydrogen (LCOH) formula with a capital recovery factor, the acceptance predicate, rungs, and a proved lemma that LCOH is monotone in electricity price. Opaque oracle (`PlantAudit`): the audited cost inputs (installed CAPEX, O&M, electricity contracts, stack replacement), metered H2 output and purity, and the lifecycle-emissions assessment (e.g. 45VH2-GREET or equivalent). Attesters: an independent financial auditor and an emissions verifier; plant must have operated for the stated period. Currency must be pinned (Hydrogen Shot uses 2020 USD). Units: USD, kg H2, kWh, years; emissions kg CO2e / kg H2; capacity MW electrical. -/ namespace OpenSpur.Problems.GreenHydrogenCost /-- Capital recovery factor r(1+r)^n / ((1+r)^n − 1). -/ noncomputable def crf (r : ℝ) (n : ℕ) : ℝ := r * (1 + r) ^ n / ((1 + r) ^ n - 1) /-- Audited plant data (oracle-attested inputs). -/ structure PlantAudit where capex : ℝ -- USD, installed discountRate : ℝ lifetimeYears : ℕ fixedOMPerYear : ℝ -- USD / yr incl. stack replacement annuity kWhPerKg : ℝ -- system specific energy, kWh / kg electricityPrice : ℝ -- USD / kWh, delivered, contracted otherVarPerKg : ℝ -- USD / kg (water, compression to spec, etc.) annualKg : ℝ -- metered kg / yr at spec purity capacityMW : ℝ operatedYears : ℝ lifecycleCO2e : ℝ -- kg CO2e / kg H2, well-to-gate auditSigned : Prop noncomputable def lcoh (p : PlantAudit) : ℝ := (p.capex * crf p.discountRate p.lifetimeYears + p.fixedOMPerYear) / p.annualKg + p.kWhPerKg * p.electricityPrice + p.otherVarPerKg structure Thresholds where maxLcoh : ℝ -- USD / kg; Hydrogen Shot: 1 maxCO2e : ℝ -- kg CO2e / kg; DOE CHPS: 4.0 minCapacityMW : ℝ -- "at scale", e.g. 100 minOperatedYears : ℝ -- e.g. 1 def hydrogenShot : Thresholds := { maxLcoh := 1, maxCO2e := 4, minCapacityMW := 100, minOperatedYears := 1 } def Solved (T : Thresholds) (p : PlantAudit) : Prop := p.auditSigned ∧ 0 < p.annualKg ∧ lcoh p ≤ T.maxLcoh ∧ p.lifecycleCO2e ≤ T.maxCO2e ∧ T.minCapacityMW ≤ p.capacityMW ∧ T.minOperatedYears ≤ p.operatedYears /-- Cheaper electricity never raises LCOH (specific energy nonnegative). -/ theorem lcoh_mono_price (p : PlantAudit) (hE : 0 ≤ p.kWhPerKg) (c : ℝ) (hc : c ≤ p.electricityPrice) : lcoh { p with electricityPrice := c } ≤ lcoh p := by unfold lcoh have := mul_le_mul_of_nonneg_left hc hE simp only linarith /-- If a plant is solved, the same plant with cheaper power is solved. -/ theorem solved_of_cheaper_power (T : Thresholds) (p : PlantAudit) (hE : 0 ≤ p.kWhPerKg) (c : ℝ) (hc : c ≤ p.electricityPrice) (h : Solved T p) : Solved T { p with electricityPrice := c } := by obtain ⟨h1, h2, h3, h4, h5, h6⟩ := h exact ⟨h1, h2, le_trans (lcoh_mono_price p hE c hc) h3, h4, h5, h6⟩ end OpenSpur.Problems.GreenHydrogenCost