Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 2 results · all verified · 2 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 2 also cleared it.

Nonconvex gradient descent and stationarity — Examples

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

None yet.

4 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Two initial intervals converge to different minima of a periodic objective

Example

Let $F (x) = 1 - \cos x$ on $R$ , and use the fixed step $α = 1$ . Its gradient is $F^{'} (x) = \sin x$ , which is $1$ -Lipschitz, and $F (x) \geq 0$ . Gradient descent is the iteration $x_{t + 1} = x_{t} - \sin x_{t}$ . Every start $x_{0} \in (0, π)$ produces a sequence converging to the global minimizer $0$ , while every start $x_{0} \in (π, 2 π)$ produces a sequence converging to the distinct global minimizer $2 π$ .

Facts & Assumptions

Given: The objective $F (x) = 1 - \cos x$ , the fixed step $α = 1$ , and an initial point in either $(0, π)$ or $(π, 2 π)$ .

[F1]

Gradient descent: with a fixed step $t_{k}$ , the update is $x_{k + 1} = x_{k} - t_{k} \nabla F (x_{k})$ .

[F2]

Gradient descent has vanishing gradients when the objective is bounded below along its iterates: for a continuously differentiable objective with $L$ -Lipschitz gradient, fixed $0 < α \leq 1 / L$ , and an objective lower bounded along the iterates, the gradient norms tend to zero.

[F3]

The derivatives of sine and cosine are cosine and minus sine: $(\cos x)^{'} = - \sin x$ , $\sin 0 = 0$ , and $\cos 0 = 1$ .

[F4]

Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ : derivatives of sums and scalar multiples are the corresponding sums and scalar multiples of derivatives, and constant functions have derivative zero.

[F5]

The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set: $f^{'} (c)$ is the limit of $(f (x) - f (c)) / (x - c)$ as $x \to c$ through $x \neq c$ ; a constant function has zero difference quotient.

[F6]

Sine and cosine are $1$ -Lipschitz on $R$ : $∣ \sin u - \sin v ∣ \leq ∣ u - v ∣$ and $∣ \cos u - \cos v ∣ \leq ∣ u - v ∣$ for all real $u, v$ .

[F7]

Pi is the first positive zero of sine: $\sin x > 0$ for $0 < x < π$ .

[F8]

The zero sets of sine and cosine and the least positive common period 2 pi: $\sin x = 0$ exactly when $x = m π$ for an integer $m$ , and both sine and cosine have period $2 π$ .

[F9]

Parity and the Pythagorean identity for sine and cosine: $\sin (- x) = - \sin x$ and $∣ \cos x ∣ \leq 1$ .

[F10]

A monotone sequence converges if and only if it is bounded: every bounded monotone real sequence converges.

Verification

1.1givenF2F3F4F5F6F8F9algebra

By [F3, F4, F5], $F^{'} (x) = \sin x$ . Then [F6] makes the gradient continuous and $1$ -Lipschitz; [F9] gives $F (x) \geq 0$ , and [F3, F8] give $F (0) = F (2 π) = 0$ . Thus the hypotheses of [F2] hold with $L = 1$ and $α = 1$ , so every trajectory has gradient norm tending to zero.

1.2givenF1F6F7F8F10algebrainduction

Suppose $x_{0} \in (0, π)$ . If $0 < x_{t} \leq x_{0}$ , [F7] gives $\sin x_{t} > 0$ , and [F6] with $v = 0$ gives $\sin x_{t} \leq x_{t}$ ; hence $0 \leq x_{t + 1} = x_{t} - \sin x_{t} < x_{t}$ . If $x_{t} = 0$ , it stays at $0$ . Induction shows $0 \leq x_{t + 1} \leq x_{t} \leq x_{0}$ , so [F10] gives a limit $ℓ \in [0, x_{0}]$ . Given $ε > 0$ , convergence gives an index after which both $∣ x_{t} - ℓ ∣ < ε / 2$ and $∣ x_{t + 1} - ℓ ∣ < ε / 2$ ; hence $∣ x_{t} - x_{t + 1} ∣ \to 0$ and, by the update, $\sin x_{t} \to 0$ . Also [F6] gives $∣ \sin x_{t} - \sin ℓ ∣ \leq ∣ x_{t} - ℓ ∣ \to 0$ , so $\sin ℓ = 0$ . By [F8], the only such zero in $[0, x_{0}]$ is $0$ , so $ℓ = 0$ .

2.1givenstep 1.2F1F6F7F8F9F10algebrainduction∎

Suppose $x_{0} \in (π, 2 π)$ . If $x_{0} \leq x_{t} < 2 π$ , put $u_{t} = 2 π - x_{t} \in (0, π)$ . By [F7, F8, F9], $\sin x_{t} = - \sin u_{t} < 0$ , and [F6] gives $- \sin x_{t} = \sin u_{t} \leq u_{t} = 2 π - x_{t}$ . Therefore $x_{t} < x_{t + 1} = x_{t} - \sin x_{t} \leq 2 π$ ; if $x_{t} = 2 π$ , it remains there. Induction gives a nondecreasing sequence bounded above by $2 π$ , so [F10] gives a limit $ℓ \in [x_{0}, 2 π]$ . Convergence implies $∣ x_{t + 1} - x_{t} ∣ \to 0$ by the same two-term estimate used in step 1.2, so $\sin u_{t} \to 0$ . Since $u_{t} = 2 π - x_{t} \to 2 π - ℓ$ , [F6] gives $∣ \sin u_{t} - \sin (2 π - ℓ) ∣ \leq ∣ u_{t} - (2 π - ℓ) ∣ \to 0$ , hence $\sin (2 π - ℓ) = 0$ . By [F8], the only such zero with $0 \leq 2 π - ℓ < 2 π - x_{0} < π$ is $0$ . Thus $ℓ = 2 π$ .

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

A gradient-descent path can be bounded below when the objective is not

Example

Let $F (x, y) = x^{2} - y^{2}$ on $R^{2}$ , start gradient descent at $w_{0} = (1, 0)$ , and use the fixed step $α = 1 / 4$ . The gradient is $(2 x, - 2 y)$ and is globally $2$ -Lipschitz. The iterates are $w_{t} = (2^{- t}, 0)$ , so $F (w_{t}) = 4^{- t} \geq 0$ and $w_{t} \to (0, 0)$ , even though $F$ is unbounded below on $R^{2}$ . The limit is stationary but is neither a local minimum nor a local maximum.

Facts & Assumptions

Given: $F (x, y) = x^{2} - y^{2}$ , $w_{0} = (1, 0)$ , and fixed step $α = 1 / 4$ .

[F1]

The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder: a derivative is a linear map whose remainder is at most $ε ∥ h ∥_{2}$ for all sufficiently small increments, for every $ε > 0$ .

[F2]

Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ : a coordinate partial derivative is the limit of the difference quotient in that coordinate direction.

[F3]

The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case: for a scalar function, the gradient vector consists of its coordinate partial derivatives.

[F4]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : $∥ (u, v) ∥_{2}^{2} = u^{2} + v^{2}$ on $R^{2}$ .

[F5]

Gradient descent: in fixed-step mode the update is $w_{t + 1} = w_{t} - α \nabla F (w_{t})$ .

[F6]

Gradient descent has vanishing gradients when the objective is bounded below along its iterates: a continuously differentiable objective on $R^{n}$ with globally $L$ -Lipschitz gradient for $L > 0$ , fixed $0 < α \leq 1 / L$ , and a lower bound along its iterates has gradient norms tending to zero along those iterates.

[F7]

For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ : if $∣ r ∣ < 1$ , then $r^{t} \to 0$ .

Verification

1.1givenF1F2F3F4algebra

For $z = (x, y)$ and $v = (h, k)$ , expansion gives $F (z + v) - F (z) - (2 x h - 2 y k) = h^{2} - k^{2}$ , whose absolute value is at most $h^{2} + k^{2} = ∥ v ∥_{2}^{2}$ . For every $ε > 0$ , this is at most $ε ∥ v ∥_{2}$ when $∥ v ∥_{2} < ε$ , so [F1] gives the total derivative. The coordinate difference quotients are $2 x + h$ and $- 2 y - k$ , so [F2, F3] give $\nabla F (x, y) = (2 x, - 2 y)$ . Therefore $∥ \nabla F (z) - \nabla F (z^{'}) ∥_{2}^{2} = 4 ∥ z - z^{'} ∥_{2}^{2}$ , so $F$ is continuously differentiable and its gradient is globally $2$ -Lipschitz.

2.1givenF5step 1.1algebrainduction

By [F5] and the gradient formula in step 1.1, $w_{t + 1} = (x_{t} / 2, 3 y_{t} / 2)$ . Starting from $(1, 0)$ , induction gives $y_{t} = 0$ and $x_{t} = 2^{- t}$ for every $t \geq 0$ .

3.1givenF6step 1.1step 2.1F7algebra∎

Step 2.1 gives $F (w_{t}) = 4^{- t} \geq 0$ and $w_{t} \to (0, 0)$ by [F7], while $F (0, s) = - s^{2}$ is unbounded below as $∣ s ∣ \to \infty$ . The gradient at the limit is zero, but $F (h, 0) = h^{2} > F (0, 0)$ and $F (0, h) = - h^{2} < F (0, 0)$ for every $h \neq 0$ , so the limit is neither a local minimum nor a local maximum. Finally $α = 1 / 4 \leq 1 / 2 = 1 / L$ and the iterates have lower bound $0$ , so [F6] applies and gives vanishing gradient norms along this path.