Provedunbiased-attentionseth-chainhardnessreduction
OV → attention estimation, fully formal: from Boolean OV vectors, constant-MSE attention estimates (≤ 1/512) at temperature d·ln(4n), majority-voted, decide OV except w.p. ≤ m(7/8)^k
For all , , , , , and , if , , , , , and (given ), then
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - x ∈ TVariables
- m, n, d range over natural numbers: the statement must hold for every choice. (
(m n d : ℕ)) - Type
- Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Type) - Fintype
- Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fintype) - f(x)Function application
- Fintype applied to Ω. Lean writes f x; papers write f(x). (
Fintype Ω) - Fin
- Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fin) - ∀For all
- The statement after the comma holds for every i, t. (
∀ i t, a i t = 0 ∨ a i t = 1) - <Less than
- 0 is strictly smaller than n. (
0 < n) - ∑Summation
- Add up w(ω) for every ω. (
∑ ω, w ω) - ≤At most
- 0 is less than or equal to w(ω). (
0 ≤ w ω) - filter
- Finset.univ.filter: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Finset.univ.filter) - =Equality
- a(i, t) and 0 are the same. (
a i t = 0) - ∨Or
- At least one holds: a(i, t) = 0, or a(i, t) = 1. (
a i t = 0 ∨ a i t = 1) - ⟹Implies
- If Fin(d), then ℝ. (Between types, A → B is the type of functions from A to B.) (
Fin d → ℝ) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - aᵇPower
- z(i, ω) − (∑ j, exp(log(4 · n)/(1 − (1 − 1/d)) · (1 − (∑ t… raised to the power 2. (
(z i ω - (∑ j, Real.exp ((Real.log (4 *…) - eˣExponential function
- e raised to the power log(4 · n)/(1 − (1 − 1/d)) · (1 − (∑ t, a(i, t) · c(j, t))…, where e ≈ 2.718. (
Real.exp ((Real.log (4 * n) / (1 - (1 -…) - logNatural logarithm
- The logarithm of 4 · n to base e: the power e must be raised to to give 4 · n. (
Real.log (4 * n)) - ∧And
- Both hold: ¬(∃ i, j, (∑ t, a(i, t) · c(j, t)) = 0) → (∀ i, ¬(k ≤ 2 · …, and (∃ i, j, (∑ t, a(i, t) · c(j, t)) = 0) → (∃ i, k ≤ 2 · car…. (
((¬ ∃ i j, ∑ t, a i t * c j t = 0) → ∀ …) - ·Multiplication
- 4 times n. (
4 * n) - ¬Not
- It is not the case that ∃ i, j, (∑ t, a(i, t) · c(j, t)) = 0. (
¬ ∃ i j, ∑ t, a i t * c j t = 0) - ∃There exists
- At least one i, j makes the statement after the comma true. (
∃ i j, ∑ t, a i t * c j t = 0) - -Subtraction
- 1 minus 1/d. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - 1 / (d : ℝ)) - a/bDivision
- 1 divided by d. In Lean, dividing by 0 gives 0. (
1 / (d : ℝ)) - (x : T)As real numbers
- d read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(d : ℝ)) - |s|Cardinality
- The number of elements of filter(r ↦ 3/8 ≤ z(i, f(r))). (
(Finset.univ.filter (fun r => 3 / 8 ≤ z…) - +Addition
- exp(log(4 · n)/(1 − (1 − 1/d))) plus ∑ j, exp(log(4 · n)/(1 − (1 − 1/d)) · (1 − (∑ t, a(i, t) ·…. (
Real.exp (Real.log (4 * n) / (1 - (1 - …) - x ↦ f(x)Function (λ-abstraction)
- The function sending r to 3/8 ≤ z(i, f(r)). Lean writes fun x => …; papers write x ↦ …. (
fun r => 3 / 8 ≤ z i (f r)) - ∏Product
- Multiply together w(f(r)) for every r. (
∏ r, w (f r))
theorem ov-to-attention-estimation {m n d : ℕ} {Ω : Type} [Fintype Ω] (a : Fin m → Fin d → ℝ) (c : Fin n → Fin d → ℝ) (ha : ∀ i t, a i t = 0 ∨ a i t = 1) (hc : ∀ j t, c j t = 0 ∨ c j t = 1) (hn : 0 < n) (hd : 0 < d) (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) (hsum : ∑ ω, w ω = 1) (z : Fin m → Ω → ℝ) (hmse : ∀ i, ∑ ω, w ω * (z i ω - (∑ j, Real.exp ((Real.log (4 * n) / (1 - (1 - 1 / (d : ℝ)))) * (1 - (∑ t, a i t * c j t) / d))) / (Real.exp (Real.log (4 * n) / (1 - (1 - 1 / (d : ℝ)))) + ∑ j, Real.exp ((Real.log (4 * n) / (1 - (1 - 1 / (d : ℝ)))) * (1 - (∑ t, a i t * c j t) / d)))) ^ 2 ≤ 1 / 512) (k : ℕ) :
∑ f ∈ Finset.univ.filter (fun f : Fin k → Ω => ¬ (((¬ ∃ i j, ∑ t, a i t * c j t = 0) → ∀ i, ¬ (k ≤ 2 * (Finset.univ.filter (fun r => 3 / 8 ≤ z i (f r))).card)) ∧ ((∃ i j, ∑ t, a i t * c j t = 0) → ∃ i, k ≤ 2 * (Finset.univ.filter (fun r => 3 / 8 ≤ z i (f r))).card))), ∏ r, w (f r) ≤ m * (7 / 8 : ℝ) ^ kThe SETH chain formalised as far as Mathlib allows. For Boolean vectors a_i, c_j ∈ {0,1}^d, set similarity x_ij = 1 − ⟨a_i, c_j⟩/d: an orthogonal pair gives x = 1, otherwise every x ≤ 1 − 1/d (Boolean inner products are 0 or ≥ 1). Any estimator of the attention rows (temperature ln(4n)/(1−s) with s = 1 − 1/d, plus one baseline key) with MSE ≤ 1/512 per row, majority-voted over k runs, decides OV correctly except with probability ≤ m(7/8)^k (embeds ua-end-to-end-reduction). Scope, stated honestly: this places constant-accuracy hardness at score range Θ(d·ln n), the regime where reductions in the style of Keles et al. and Alman–Song already apply, so the substance is likely folklore and the contribution is the machine-checked chain. Reaching the conjectured range ln n needs Rubinstein's MA-protocol gap amplification, which requires coding-theory machinery Mathlib lacks; SETH itself (a statement about running time) cannot be stated in Mathlib.
How it was proved
- Proved
- 5 October 2026
- By
- Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
- Checked by
- Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
- Axioms
- Classical.choice, Quot.sound, propext
- Proof
- 224 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.