Predicting molecular biomarkers / outcomes from H&E whole-slide images

On the public HEST-Benchmark (9 cancer/organ tasks, 50 genes each, predicted from H&E patches) the best of 25 pathology foundation models, Bioptimus H-Optimus-1, averages Pearson 0.4229 (ResNet50 baseline 0.3252) as of Apr 2026; deployed H&E-to-MSI products such as MSIntuit are validated as pre-screening tools, not replacements for molecular testing.

Source: github.com

No prize money is attached to this problem.

import Mathlib

/-!
# Predicting molecular biomarkers from H&E whole-slide images

Example targets: MSI/dMMR status in colorectal cancer, HRD status in breast/ovarian
cancer, ISUP grade (PANDA). This file covers binary biomarkers.

Concrete in Lean: the submission (slide → score), AUROC over a finite labelled set as
the Mann–Whitney statistic (ties count ½), sensitivity at a fixed decision threshold,
and a Prop requiring the bar on EVERY external cohort (not the development cohort).

Opaque oracle (`Cohort`): the hidden slides, their ground-truth labels from the
reference molecular assay (PCR/IHC for MSI, genomic scar assay for HRD), and the
guarantee that cohorts come from institutions/scanners not used in training.
Attesters: the data custodians (hospital consortia / challenge organisers) who hold the
labels and run the frozen model.

Units: AUROC, sensitivity, specificity dimensionless in [0, 1].
Indicative bars (MSI screening literature): AUROC ≥ 0.90, sensitivity ≥ 0.95 at a
pre-registered threshold, specificity ≥ 0.5 there (rule-out use).
-/

namespace OpenSpur.Problems.PathologyBiomarker

/-- Opaque handle to a whole-slide image (content-addressed hash). -/
structure Slide where
  hash : String

abbrev Model := Slide → ℝ

noncomputable section

/-- AUROC = P(score(pos) > score(neg)) + ½ P(tie), over all positive/negative pairs. -/
def auroc (pos neg : List ℝ) : ℝ :=
  (((pos.flatMap fun p => neg.map fun q =>
      if q < p then (1 : ℝ) else if q = p then 1 / 2 else 0)).sum)
    / ((pos.length : ℝ) * neg.length)

def sensitivity (pos : List ℝ) (t : ℝ) : ℝ :=
  ((pos.filter fun s => decide (t ≤ s)).length : ℝ) / pos.length

def specificity (neg : List ℝ) (t : ℝ) : ℝ :=
  ((neg.filter fun s => decide (s < t)).length : ℝ) / neg.length

/-- One held-out external cohort (oracle). -/
structure Cohort where
  positives : List Slide
  negatives : List Slide

structure Thresholds where
  minAuroc : ℝ
  minSens : ℝ
  minSpec : ℝ
  minPos : ℕ       -- e.g. 30 positive cases per cohort
  minNeg : ℕ

def Solved (T : Thresholds) (cohorts : List Cohort) (m : Model) (t : ℝ) : Prop :=
  2 ≤ cohorts.length ∧            -- at least two independent external cohorts
  ∀ c ∈ cohorts,
    T.minPos ≤ c.positives.length ∧ T.minNeg ≤ c.negatives.length ∧
    T.minAuroc ≤ auroc (c.positives.map m) (c.negatives.map m) ∧
    T.minSens ≤ sensitivity (c.positives.map m) t ∧
    T.minSpec ≤ specificity (c.negatives.map m) t

def msiScreen : Thresholds :=
  { minAuroc := 0.9, minSens := 0.95, minSpec := 0.5, minPos := 30, minNeg := 100 }

def rung (T : Thresholds) (k : ℕ) : Thresholds :=
  { T with minAuroc := T.minAuroc + (k : ℝ) / 100 }

end

theorem rung_mono (T : Thresholds) (cs : List Cohort) (m : Model) (t : ℝ) {j k : ℕ}
    (hjk : j ≤ k) (h : Solved (rung T k) cs m t) : Solved (rung T j) cs m t := by
  have hc : (j : ℝ) ≤ k := by exact_mod_cast hjk
  refine ⟨h.1, fun c hc' => ?_⟩
  obtain ⟨a, b, d, e, f⟩ := h.2 c hc'
  refine ⟨a, b, ?_, e, f⟩
  simp only [rung] at d ⊢
  linarith

end OpenSpur.Problems.PathologyBiomarker

• HEST-1k (1,276 paired spatial transcriptomics + H&E samples) and HEST-Benchmark
• CHIMERA challenge (MICCAI 2025): prostate/bladder recurrence and BCG response from H&E + MRI + transcriptomics
• PANDA prostate cancer grading challenge (Kaggle)
• Owkin Phikon-v2 pathology foundation model
• Bioptimus H-optimus-1 pathology foundation model (gated)