Problem
Compact, specific gene editors deliverable in vivo
A single adeno-associated virus (AAV) vector can carry only about 4.7 kb of DNA, and the SpCas9 coding sequence alone consumes roughly 4.1 kb, leaving no room for promoters, guide RNA and regulatory elements; the same size pressure applies to lipid-nanoparticle mRNA payloads. The commercial consequence is that almost every approved or clinical-stage CRISPR medicine edits the liver ex vivo or via LNP-to-hepatocyte delivery, so muscle, CNS, lung and immune-cell indications, which are the larger markets, remain out of reach. A solution is an editor whose coding sequence plus guide and promoter fit in one AAV (or one LNP payload) while matching or beating SpCas9 on-target activity and holding off-target editing near the detection floor. Concretely: Profluent's AI-designed OpenCRISPR-1 reached 48.3% on-target editing with 0.32% off-target editing versus 6.1% for SpCas9 (a 95% reduction), but it is still a Cas9-scale protein; Mammoth's NanoCas is ultracompact enough for single-AAV delivery but its extrahepatic editing results are preclinical. SOLVED would mean a single-vector-deliverable editor demonstrating therapeutically meaningful editing (tens of percent of target alleles) in a non-liver tissue in vivo, with off-target edits below ~0.1% and a clinical dataset behind it.
Funding
Raised by the 7 companies working on it, 1 undisclosed.
Why it is still open
The best-characterised AI-designed editor published to date (OpenCRISPR-1, Nature, July 2025) matches SpCas9 on-target activity and cuts off-target editing by ~95%, but it is still a Cas9-scale protein, so it does not solve the AAV cargo problem; as of Sep 2026 the compact editors that do fit one AAV (e.g. Mammoth's NanoCas) have only preclinical extrahepatic editing data, and no compact editor has clinical in vivo extrahepatic efficacy.
Source: pubmed.ncbi.nlm.nih.gov
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
No prize money is attached to this problem.
What counts as solved
import Mathlib.Data.Real.Basic import Mathlib.Tactic.Linarith import Mathlib.Tactic.NormNum /-! # Compact, specific gene editors deliverable in vivo What is formalized: the *acceptance arithmetic* only. A candidate is a record of declared sizes; whether it counts as solved is a conjunction of numeric thresholds over quantities that Lean cannot compute. Concrete here: the packaging budget. An AAV vector has a single-stranded genome limit of about 4.7 kb, and the editor's expression cassette must fit inside it together with its regulatory elements, so `cassetteKb ≤ cargoLimitKb` is plain arithmetic on declared kilobase counts. Opaque oracle (`Assay`): on-target editing efficiency, unbiased off-target count, and the delivered-tissue editing fraction. These come from wet-lab measurement, not from this file, and no protocol, sequence or design guidance is expressed or implied anywhere here. Who must attest: an independent laboratory running a pre-registered protocol on a named target locus in a named animal model, reporting (i) on-target editing efficiency by amplicon sequencing, (ii) genome-wide off-target sites by an unbiased detection method, (iii) the fraction of target-tissue cells edited after systemic dosing. The `Assay` record is that laboratory's signed report. Units: `cassetteKb`, `cargoLimitKb` in kilobases (kb). Efficiencies and fractions are dimensionless fractions in [0,1]. `offTargetSites` is a count of detected off-target loci above the method's detection threshold. Checked with Lean 4.33.0 / Mathlib using: lake env lean <absolute-path-to-this-file> -/ namespace OpenSpur.Problems.GeneEditorDesign /-- Declared, checkable size data for one editor construct. -/ structure Candidate where /-- Length of the full expression cassette to be packaged, in kb. -/ cassetteKb : ℝ /-- Number of separate vectors the construct requires when dosed. -/ vectorCount : Nat /-- Laboratory-measured quantities. Lean computes none of these. -/ structure Assay where /-- Fraction of alleles edited at the intended locus. -/ onTargetEfficiency : ℝ /-- Off-target loci detected genome-wide by an unbiased method. -/ offTargetSites : Nat /-- Fraction of target-tissue cells edited after systemic dosing. -/ tissueEditedFraction : ℝ /-- The report is a pre-registered, independently run protocol. -/ preRegistered : Prop /-- Off-target detection used an unbiased genome-wide method. -/ unbiasedOffTargetMethod : Prop /-- Packaging budget and outcome thresholds. -/ structure Thresholds where /-- Single-vector cargo limit; ~4.7 kb for AAV. -/ cargoLimitKb : ℝ minOnTarget : ℝ maxOffTargetSites : Nat minTissueEdited : ℝ /-- The AAV single-stranded packaging limit, in kb. -/ def aavCargoLimitKb : ℝ := 4.7 /-- Concrete: the cassette fits one vector within the cargo limit. -/ def FitsSingleVector (T : Thresholds) (c : Candidate) : Prop := c.vectorCount = 1 ∧ c.cassetteKb ≤ T.cargoLimitKb /-- Acceptance predicate: packaging is checked, outcomes are attested. -/ def Solved (T : Thresholds) (c : Candidate) (a : Assay) : Prop := FitsSingleVector T c ∧ a.preRegistered ∧ a.unbiasedOffTargetMethod ∧ T.minOnTarget ≤ a.onTargetEfficiency ∧ a.offTargetSites ≤ T.maxOffTargetSites ∧ T.minTissueEdited ≤ a.tissueEditedFraction /-- A tightening family: rung `k` demands a higher edited tissue fraction, fewer tolerated off-target loci is not modelled here as it is a Nat floor. -/ def Rung (k : ℕ) : Thresholds where cargoLimitKb := aavCargoLimitKb minOnTarget := 0.5 maxOffTargetSites := 1 minTissueEdited := 0.1 + 0.05 * (k : ℝ) /-- Rungs tighten monotonically in the tissue-editing requirement. -/ theorem rung_minTissueEdited_mono {j k : ℕ} (h : j ≤ k) : (Rung j).minTissueEdited ≤ (Rung k).minTissueEdited := by have : (j : ℝ) ≤ (k : ℝ) := Nat.cast_le.mpr h have h5 : (0 : ℝ) ≤ 0.05 := by norm_num simp only [Rung] have := mul_le_mul_of_nonneg_left this h5 linarith /-- Solving a higher rung implies solving every lower rung. -/ theorem solved_rung_mono {j k : ℕ} (h : j ≤ k) (c : Candidate) (a : Assay) : Solved (Rung k) c a → Solved (Rung j) c a := by intro hs obtain ⟨hfit, hpre, hunb, hon, hoff, htis⟩ := hs refine ⟨?_, hpre, hunb, ?_, ?_, ?_⟩ · exact ⟨hfit.1, hfit.2⟩ · exact hon · exact hoff · exact le_trans (rung_minTissueEdited_mono h) htis end OpenSpur.Problems.GeneEditorDesign
Public resources
- OpenCRISPR (AI-generated gene editing systems, code + weights)
- Design of highly functional genome editors by modelling CRISPR-Cas sequences (Nature 2025)
- Profluent E1 protein representation model family (Hugging Face)
- Evo 2 genome foundation model, 40B (Arc Institute, Hugging Face)
- Arc Institute Bridge RNA Design Tool (programmable recombinase targeting)