Problem
Sorbents / catalysts meeting carbon-capture and conversion targets
Direct air capture and point-source capture both hinge on a material: a sorbent that binds CO2 selectively from a humid, CO2-dilute gas stream and then gives it back at low regeneration energy over thousands of cycles, or a catalyst that converts captured CO2 into a saleable product. Cost is the whole commercial story - Climeworks, the largest DAC operator, sits around $1,000 per tonne today and targets $250-350/t capture and $400-600/t net removal only by 2030, while buyers, policy models and the $100/t aspiration used across the field need roughly an order of magnitude improvement. The candidate space (MOFs, amine-functionalised solids, covalent frameworks) is effectively unbounded, which is why the public effort has gone into screening data: ODAC23 covered ~8,400 MOFs with 38M DFT calculations, and ODAC25 (Meta FAIR, Georgia Tech, CuspAI, Aug 2025) extends this to over 100 million data points. SOLVED is not 'a new MOF' but a sorbent with validated CO2 working capacity under realistic humidity, cycle stability over thousands of adsorption/desorption cycles, and a measured regeneration energy consistent with sub-$100/t capture at scale - or, on the conversion side, a catalyst whose predicted adsorption energies (Open Catalyst / OC20-style) survive experimental confirmation at industrially relevant current densities.
Funding
Raised by the 6 companies working on it, 1 undisclosed.
Why it is still open
The best-funded DAC operator's costs are still roughly $1,000 per tonne of CO2, and its next-generation technology only targets $250-350/t captured ($400-600/t net removal) by 2030 - so the sorbent-driven step change to the ~$100/t level that the field's economics assume has not happened as of Sep 2026; the ODAC23/ODAC25 datasets exist precisely because the promising sorbents have not yet been identified.
Source: canarymedia.com
Who is working on it
Also active
Funding for these is not counted: the problem is a small part of what they do, or they contribute data and tools.
Prizes
| Prize | Status | Pays for | Amount |
|---|---|---|---|
| XPRIZE Carbon Removal | Awarded | Solving | $100M |
| U.S. DOE Carbon Dioxide Removal Purchase Pilot Prize (incl. the DAC commercial track) | Announced | Solving | $35M |
What counts as solved
import Mathlib.Data.Real.Basic import Mathlib.Tactic.Linarith import Mathlib.Tactic.NormNum /-! # Sorbents / catalysts meeting carbon-capture and conversion targets Concrete here: the **cost and net-removal arithmetic**. Given audited annual figures, net removal is gross captured CO₂ minus life-cycle emissions of the capture plant, and cost per net tonne is total annualised spend divided by net removed tonnes. Both are ordinary arithmetic once the figures exist, and this file defines them, including the division-by-zero guard (`0 < netRemoved`). Opaque oracle (`Audit`): the measured quantities themselves — gross CO₂ captured, life-cycle emissions, capex amortisation and opex, measured sorbent working capacity, regeneration energy, and retained capacity after cycling. These come from an operating plant plus a third-party life-cycle assessment, never from Lean. Who must attest: an independent MRV auditor of the XPRIZE-Carbon-Removal kind (verified tonnes removed and durably stored, with a full life-cycle boundary), plus a lab report of the sorbent's working capacity, regeneration duty and cycling durability under the declared feed condition. The `Audit` record is their joint signed report. Units: `grossCapturedTonnes`, `lifecycleEmissionsTonnes`, `netRemoved` in tonnes CO₂ per year; `annualisedCostUsd` in USD per year; cost thresholds in USD per net tonne CO₂; `workingCapacity` in mmol CO₂ per gram of sorbent; `regenEnergy` in GJ per tonne CO₂; `retainedCapacityFraction` dimensionless in [0,1] after `cycles` adsorption/desorption cycles; `feedConcentrationPpm` in ppm (~420 ppm for direct air capture). Checked with Lean 4.33.0 / Mathlib using: lake env lean <absolute-path-to-this-file> -/ namespace OpenSpur.Problems.CarbonCaptureMaterials /-- Audited plant-year figures plus the sorbent's measured performance. -/ structure Audit where grossCapturedTonnes : ℝ lifecycleEmissionsTonnes : ℝ annualisedCostUsd : ℝ workingCapacity : ℝ regenEnergy : ℝ cycles : ℕ retainedCapacityFraction : ℝ feedConcentrationPpm : ℝ /-- Storage durability of the removed CO₂ was verified (≥ 100 years). -/ durableStorageVerified : Prop /-- Life-cycle boundary and tonnage were verified by an independent auditor. -/ independentlyAudited : Prop /-- Net tonnes CO₂ removed per year: concrete, from audited figures. -/ def netRemoved (A : Audit) : ℝ := A.grossCapturedTonnes - A.lifecycleEmissionsTonnes /-- Cost in USD per net tonne removed; only meaningful when `0 < netRemoved`. -/ noncomputable def costPerNetTonne (A : Audit) : ℝ := A.annualisedCostUsd / netRemoved A /-- Targets a board would pay against. -/ structure Thresholds where /-- USD per net tonne, e.g. the 100 $/t direct-air-capture target. -/ maxCostPerTonne : ℝ /-- Minimum demonstrated scale, net tonnes per year (XPRIZE used 1000 t/yr). -/ minNetRemoved : ℝ /-- Minimum sorbent working capacity, mmol/g. -/ minWorkingCapacity : ℝ /-- Maximum regeneration duty, GJ per tonne CO₂. -/ maxRegenEnergy : ℝ /-- Cycles the sorbent must survive. -/ minCycles : ℕ /-- Capacity fraction still retained after those cycles. -/ minRetainedFraction : ℝ /-- Feed the plant must run on; DAC means ambient air, ~420 ppm. -/ maxFeedConcentrationPpm : ℝ /-- Ambient-air CO₂ concentration, ppm, as of the mid-2020s. -/ def ambientCo2Ppm : ℝ := 420 /-- Acceptance predicate. Cost and scale are computed from audited figures; the figures themselves are attested, not derived. -/ def Solved (T : Thresholds) (A : Audit) : Prop := A.independentlyAudited ∧ A.durableStorageVerified ∧ A.feedConcentrationPpm ≤ T.maxFeedConcentrationPpm ∧ T.minNetRemoved ≤ netRemoved A ∧ 0 < netRemoved A ∧ costPerNetTonne A ≤ T.maxCostPerTonne ∧ T.minWorkingCapacity ≤ A.workingCapacity ∧ A.regenEnergy ≤ T.maxRegenEnergy ∧ T.minCycles ≤ A.cycles ∧ T.minRetainedFraction ≤ A.retainedCapacityFraction /-- Rung `k` holds the engineering bars fixed and tightens only the price: 400 $/t at k = 0, falling by 50 $/t per rung, floored implicitly by the user's choice of `k` (rungs beyond k = 6 demand a negative price and are unreachable). -/ def Rung (k : ℕ) : Thresholds where maxCostPerTonne := 400 - 50 * (k : ℝ) minNetRemoved := 1000 minWorkingCapacity := 1 maxRegenEnergy := 4 minCycles := 1000 minRetainedFraction := 0.9 maxFeedConcentrationPpm := ambientCo2Ppm /-- The price bar tightens monotonically along the rungs. -/ theorem rung_price_antitone {j k : ℕ} (h : j ≤ k) : (Rung k).maxCostPerTonne ≤ (Rung j).maxCostPerTonne := by have hjk : (j : ℝ) ≤ (k : ℝ) := Nat.cast_le.mpr h simp only [Rung] linarith /-- Hitting a higher rung's price implies hitting every lower rung. -/ theorem solved_rung_mono {j k : ℕ} (h : j ≤ k) (A : Audit) : Solved (Rung k) A → Solved (Rung j) A := by intro hs obtain ⟨h1, h2, h3, h4, h5, h6, h7, h8, h9, h10⟩ := hs exact ⟨h1, h2, h3, h4, h5, le_trans h6 (rung_price_antitone h), h7, h8, h9, h10⟩ end OpenSpur.Problems.CarbonCaptureMaterials
Public resources
- Open DAC 2023 (ODAC23): 38M DFT calculations on 8,400+ MOFs with adsorbed CO2/H2O
- Open DAC 2025 (ODAC25) dataset, 100M+ data points (Meta FAIR / Georgia Tech / CuspAI)
- LeMat-Cat (OC20-derived catalysis/adsorption datasets, Entalpic)
- MofasaDB: 200k+ de novo generated MOFs with relaxed structures (Orbital)
- kUPS interatomic potential, JAX export (CuspAI)