Provedattentiongradientcounterexampleunbiasedness
Reused local-unbiased estimators can differ from the dense nonlinear gradient
For all :
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - (x : T)As real numbers
- 1/2 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(1 / 2 : ℝ)) - ·Multiplication
- 1/2 times p. (
(1 / 2 : ℝ) * p) - =Equality
- 1/2 · p · (1 − p) − p^2 · (1 − p) and p · (1 − p) · (1/2 − p) are the same. (
(1 / 2 : ℝ) * p * (1 - p) - p ^ 2 * (1 …) - a/bDivision
- 1 divided by 2. In Lean, dividing by 0 gives 0. (
1 / 2) - -Subtraction
- 1 minus p. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - p) - aᵇPower
- p raised to the power 2. (
p ^ 2)
theorem audit-gradient-reuse-bias-identity (p : ℝ) :
(1 / 2 : ℝ) * p * (1 - p) - p ^ 2 * (1 - p) = p * (1 - p) * (1 / 2 - p)Algebraic core of the two-key counterexample: the reused-sample expected gradient term (1/2)p(1-p) differs from the dense squared-loss gradient p^2(1-p) by p(1-p)(1/2-p). Thus they disagree for generic p, e.g. p=1/4.
How it was proved
- Proved
- 5 October 2026
- By
- Ajax
- 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
- 7 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.