Human-level abstract reasoning on ARC-AGI

As of Sep 2026 the problem is split. Closed frontier models have largely closed the gap on the semi-private sets: ARC Prize verified OpenAI GPT-6 Astra at 99.9% on ARC-AGI-3 semi-private with the 'Provider Adapter' harness (~$19K) and 62.7% with the standard harness (2026-09-03), and third-party trackers report >90% on ARC-AGI-2. The efficiency-constrained, open-source version that the prize pays for is still unsolved. ARC Prize 2025's best Kaggle ARC-AGI-2 private score was 24.03%, and the ARC-AGI-3 Milestone-1 winners (June 2026) were small local open models. The $700K ARC-AGI-3 grand prize is unclaimed; 2026 final submissions are due 2026-11-02 and results come 2026-12-04.

Source: arcprize.org

import Mathlib.Data.Real.Basic
import Mathlib.Data.Finset.Card
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum

/-!
# Human-level abstract reasoning on ARC-AGI

Almost everything here is concrete. A grid is a list of rows of colour indices;
a task carries its demonstration pairs and its hidden test pairs. A solver is a
function from an input grid to an ordered list of at most two candidate output
grids (the ARC two-attempt rule). Solving a task is *exact grid equality*: for
every hidden test pair, the expected output occurs in the solver's candidate
list, and that list has length ≤ 2. Scoring is integer arithmetic:
`100 * solved ≥ pass * total` avoids any division.

Opaque oracle: only the private evaluation set itself (the tasks and their hidden
outputs, which the host never publishes) and the resource attestations — that the
solver ran within the declared compute and time budget, offline, without access
to the private set during development.

Who must attest: the prize host, which holds the private tasks, runs the
submitted solver in its own sealed container, and publishes the count of tasks
passed and the measured compute. `accepted` is the set of task indices the host
certifies; the predicate then forces exact-match evidence for each of them.

Units: grid entries are colour indices (0–9 in ARC); `passPercent` is an integer
percentage of tasks; attempts are counted per test input.

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

namespace OpenSpur.Problems.AbstractReasoningArc

/-- A grid: rows of colour indices. Equality is exact, cell by cell. -/
abbrev Grid := List (List ℕ)

/-- One task: demonstration pairs, plus hidden input/output test pairs. -/
structure Task where
  demos : List (Grid × Grid)
  tests : List (Grid × Grid)

/-- A solver proposes an ordered list of candidate outputs for an input grid. -/
abbrev Solver := Grid → List Grid

/-- Concrete: every hidden test pair is matched exactly within `maxAttempts`
candidates. -/
def SolvesTask (maxAttempts : ℕ) (s : Solver) (t : Task) : Prop :=
  ∀ p ∈ t.tests, (s p.1).length ≤ maxAttempts ∧ p.2 ∈ s p.1

/-- The private evaluation set and its resource attestations. -/
structure PrivateEval (n : ℕ) where
  task : Fin n → Task
  /-- The set was never exposed to the submission's development loop. -/
  setUnseen : Prop
  /-- The run stayed inside the declared compute and wall-clock budget. -/
  withinComputeBudget : Prop
  /-- The run was offline: no network, no external model calls. -/
  offline : Prop

/-- Pass bar and attempt allowance. -/
structure Thresholds where
  /-- Required percentage of private tasks solved, e.g. 85. -/
  passPercent : ℕ
  /-- Attempts allowed per test input; ARC allows 2. -/
  maxAttempts : ℕ

/-- The ARC two-attempt rule. -/
def arcMaxAttempts : ℕ := 2

/-- Acceptance predicate. `accepted` is the host-certified set of solved tasks;
each member must exhibit exact-match outputs within the attempt allowance. -/
def Solved {n : ℕ} (T : Thresholds) (E : PrivateEval n) (s : Solver)
    (accepted : Finset (Fin n)) : Prop :=
  E.setUnseen ∧
  E.withinComputeBudget ∧
  E.offline ∧
  (∀ i ∈ accepted, SolvesTask T.maxAttempts s (E.task i)) ∧
  T.passPercent * n ≤ 100 * accepted.card

/-- Rung `k` asks for `50 + 5k` percent of the private set, two attempts. -/
def Rung (k : ℕ) : Thresholds where
  passPercent := 50 + 5 * k
  maxAttempts := arcMaxAttempts

/-- The pass bar tightens monotonically along the rungs. -/
theorem rung_pass_mono {j k : ℕ} (h : j ≤ k) :
    (Rung j).passPercent ≤ (Rung k).passPercent := by
  simp only [Rung]
  exact Nat.add_le_add_left (Nat.mul_le_mul_left 5 h) 50

/-- Solving a higher rung implies solving every lower rung. -/
theorem solved_rung_mono {n j k : ℕ} (h : j ≤ k) (E : PrivateEval n) (s : Solver)
    (accepted : Finset (Fin n)) :
    Solved (Rung k) E s accepted → Solved (Rung j) E s accepted := by
  intro hs
  obtain ⟨h1, h2, h3, h4, h5⟩ := hs
  refine ⟨h1, h2, h3, h4, ?_⟩
  have hb : (Rung j).passPercent * n ≤ (Rung k).passPercent * n :=
    Nat.mul_le_mul_right n (rung_pass_mono h)
  exact le_trans hb h5

/-- Certifying fewer tasks can only lower the score: the accepted set's
contribution is monotone under inclusion. -/
theorem accepted_card_mono {n : ℕ} {a b : Finset (Fin n)} (h : a ⊆ b) :
    100 * a.card ≤ 100 * b.card :=
  Nat.mul_le_mul_left 100 (Finset.card_le_card h)

end OpenSpur.Problems.AbstractReasoningArc

• ARC-AGI-3 benchmark (interactive environments)
• ARC-AGI-2 benchmark
• ARC Prize leaderboard (verified; systems under $10K)
• Kaggle: ARC Prize 2026 - ARC-AGI-3
• Kaggle: ARC Prize 2026 - ARC-AGI-2
• ARC Prize 2025 Technical Report (arXiv 2601.10904)