Machine Learning

Why initialization matters for transfer learning

Transfer learning starts with a representation learned on an earlier task and adapts it to a new one. Two common choices are linear probing, which changes only the final linear predictor, and fine-tuning, which changes the representation as well. These procedures optimize related training objectives, but their behavior away from the training data can differ. Kumar and coauthors study this distinction through two-layer linear networks, alongside experiments with nonlinear networks. This mission formalizes their perfect-feature LP-FT result, rather than the empirical claims or the general imperfect-feature comparison. See Section 3.4, Proposition 3.7, PDF p. 10.

LP-FT first learns a head by linear probing and then uses that head to initialize full fine-tuning. The perfect-feature setting isolates the effect of head initialization: the representation already contains exactly the features needed to predict the labels, but the head initially need not use them correctly. The mathematical question is whether joint training preserves or loses the representation's ability to predict outside the observed training subspace.

Linear predictors, training data, and OOD loss

An input is a vector $x\in\mathbb R^d$. A feature extractor is a matrix $B\in\mathbb R^{k\times d}$, and a head is a vector $v\in\mathbb R^k$. Together they predict $v^\top Bx$, with effective weight vector $B^\top v$. The fixed matrix $X\in\mathbb R^{n\times d}$ contains the $n$ training inputs as rows. Their span is $S=\operatorname{rowspace}(X)$, with dimension $m$.

The ground truth has orthonormal-row features $B_\star$ and a nonzero head $v_\star$. Write $w_\star=B_\star^\top v_\star$ and $Y=Xw_\star$. Perfect pretrained features mean $B_0=UB_\star$ for an orthogonal matrix $U$. The corresponding aligned head is $u=Uv_\star$. The dimensions satisfy $1\le k\le m$ and $m+k<d$.

The two geometric assumptions require the orthogonal projections from $R_0=\operatorname{rowspace}(B_0)$ into $S$ and into $S^\perp$ to be injective. In this dimension regime these are exactly the positive largest-principal-angle cosine conditions used by the paper. They demand more than two subspaces having some nonorthogonal directions. The Lean definition spells out injectivity of $v\mapsto\Pi_T B_0^\top v$ for each $T\in\{S,S^\perp\}$. See Definition 3.2 and Appendix A.1, PDF pp. 7 and 22-23.

An out-of-distribution law $\mu$ is any probability measure on $\mathbb R^d$ with a finite second moment and positive-definite uncentered second-moment matrix $\Sigma=\mathbb E_\mu[xx^\top]$. Its mean need not be zero. Define

$$L_{\rm OOD}(v,B)=\mathbb E_{x\sim\mu} [(v^\top Bx-w_\star^\top x)^2].$$

Both training methods use the unnormalized loss $\widehat L(v,B)=\|XB^\top v-Y\|_2^2$. Fine-tuning follows its gradient flow in both parameters; linear probing keeps $B=B_0$. Time is real and nonnegative. These are the paper's equations (3.2)-(3.3), PDF p. 6.

Formalization targets

The goal is Proposition 3.7 in an explicit nonzero-signal regime. For $\sigma>0$, initialize an FT head with independent Gaussian coordinates, $v_0\sim\mathcal N(0,\sigma^2I_k)$. Establish

$$\Pr\!\left[\forall t\ge0,\quad L_{\rm OOD}(v_{\rm FT}(t),B_{\rm FT}(t))>0\right]=1.$$

Linear probing, from any initial head, must converge to $u$. Fine-tuning initialized at its limit must satisfy

$$v_{\rm LP}(t)\longrightarrow u,\qquad \forall t\ge0,\quad L_{\rm OOD}(v_{\rm LP\text{-}FT}(t),B_{\rm LP\text{-}FT}(t))=0.$$

The probability-one event applies to all times simultaneously. The goal also asserts existence of the relevant global flows; a conditional claim about a possibly nonexistent trajectory would not suffice. The statement does not assert a numerical error lower bound or a positive time-infimum.

Seven milestones supply the supporting results: global flow existence and FT uniqueness; unchanged features orthogonal to the training span; the balancedness invariant; the second-moment identity for OOD risk; almost-sure Gaussian head misalignment; exact LP recovery; and stationarity after LP initialization. The principal source is Appendices A.2 and A.7, PDF pp. 23-31 and 45-47.

What the result establishes

The result distinguishes two initializations of the same joint-training procedure. In this idealized setting, a head obtained by linear probing gives zero OOD loss throughout subsequent fine-tuning, while a Gaussian head almost surely has positive OOD loss at every finite time. The conclusion concerns population squared prediction error, not classification accuracy or a finite test-set estimate.

The paper establishes the mathematical claim; this mission asks for a Lean proof of the stated model and result. The scope is deliberately limited to perfect pretrained features. It does not claim an LP-FT upper bound for imperfect features, which the authors identify as a further challenge in Section 3.4, PDF p. 10. A completed development would also provide reusable components for finite dimensional gradient flows, factorized linear models, and population risk.

Why the proof needs the training dynamics

The training loss alone does not select a unique effective predictor in an overparameterized problem. Knowing that a predictor fits the observed examples therefore does not determine its OOD loss. Formalization must track the head and feature extractor together, and it must distinguish parameter stationarity from a claim that a derivative happens to vanish at one time. The Gaussian conclusion also requires one event controlling an uncountable set of times; separate probability-one statements for individual times would be weaker.

Formalization scope and conventions

Vectors use Mathlib's finite dimensional real Euclidean spaces. Matrices are represented as continuous linear maps, with Euclidean adjoints and operator norms. The feature update is written explicitly as the Frobenius-gradient equation; it is not a gradient with respect to the operator norm. Differentiability is imposed within $[0,\infty)$, including the right derivative at zero.

The dimensions, nonzero target, positive Gaussian scale, finite second moments, and projection injectivity are explicit. The nonzero target restricts the formalization to the regime of the Gaussian alignment argument in Lemma A.12; $k\le m$ makes the identifiability condition used in Proposition A.20 precise. The random-head law is the scaled standard Gaussian measure. No randomness of the fixed training matrix or independence from an additional data draw is assumed.

The model contains no assumed convergence, invariant, or desired risk bound. Each of those is a theorem obligation. The well-posedness milestone makes explicit an analytic prerequisite of the source's flow notation. The risk milestone uses the identity in (A.29)-(A.32), avoiding the reversed inequality printed in (A.28). The quantitative constant in Theorem 3.3 is outside this mission. Source-aligned proofs and the supporting analysis infrastructure are welcome; changing the learning rule or assuming a milestone inside the model would change the task.

Selected references

• Ananya Kumar, Aditi Raghunathan, Robbie Jones, Tengyu Ma, and Percy Liang, Fine-Tuning can Distort Pretrained Features and Underperform Out-of-Distribution, ICLR 2022, arXiv:2202.10054v1. Main target: Section 3.4, Proposition 3.7, PDF p. 10, equations (3.10)-(3.11); proof: Appendix A.7, PDF pp. 45-47, Proposition A.20 and (A.208)-(A.218). Supporting invariants: Appendix A.2, PDF p. 24, Lemmas A.3-A.4, equations (A.15)-(A.20). Gaussian alignment: Appendix A.3, PDF pp. 34-35, Lemmas A.11-A.12.

Why the geometry of a minimum needs a parameter convention

A trained neural network is used through its predictions, while its parameters are the coordinates in which training takes place. Distinct parameter vectors can describe exactly the same prediction function. A proposed explanation of generalization based on the shape of the parameter-space loss therefore needs to account for these equivalences. This mission concerns Hessian sharpness: the spectral norm of the matrix of second derivatives of the loss at a minimum. The question is whether that number is intrinsic to the predictor or can change without changing any prediction.

Dinh, Pascanu, Bengio, and Bengio establish that, for a one-hidden-layer rectified network, every sufficiently differentiable critical minimum with nonzero Hessian has equivalent parameterizations of arbitrarily large Hessian sharpness. The formalization target is their Section 4.2, Theorem 4, PDF pp. 5–6. The goal theorem and both supporting milestones now have accepted Lean proofs on Prove2Me. This public research-paper mission is complete.

The immediate historical sequence is:

• 2016–2017: Keskar and collaborators reported numerical evidence relating large-batch training, sharp minima, and a generalization gap. This is empirical context, not an assumption or a theorem to be proved in this mission. ICLR 2017 paper.
• March 2017: Dinh and collaborators released a mathematical analysis of parameter symmetries and several flatness measures. The fixed source for this mission is their May 2017 revision, arXiv version 2, which determines the theorem numbering and PDF page citations. Version history.

Networks, losses, and reciprocal layer scaling

Fix positive integers $d$ and $h$, the input dimension and hidden width. Let $W\in\mathbb R^{d\times h}$ and $v\in\mathbb R^h$ be the network's weights. For an input $x\in\mathbb R^d$, define

$$f_{W,v}(x)=\sum_{j=1}^h \max\!\left(\sum_{i=1}^d x_iW_{ij},0\right)v_j.$$

This is a bias-free network with one hidden layer, rectified activation, and a scalar linear output. Its parameter vector $\theta=(W,v)$ has $n=dh+h$ coordinates and the Euclidean norm. A function-based loss is a real-valued functional $\ell$ of the entire prediction function, giving $L(\theta)=\ell(f_\theta)$. The Hessian targets assume $L$ is continuous. These conventions come from Sections 2–3, PDF pp. 2–4, Definition 3.

Two parameters are observationally equivalent if their predictions agree on every input. For a positive real number $\alpha$, the layer scaling is

$$T_\alpha(W,v)=(\alpha W,\alpha^{-1}v).$$

The definition rescales the incoming and outgoing weights in opposite ways. It is the transformation in Section 3, Definition 5, PDF p. 4.

Write $DL(\theta)$ for the first Fréchet derivative and $H_L(\theta)=D(DL)(\theta)$ for the second derivative. The local differentiability condition requires $L$ to be differentiable throughout a neighborhood of $\theta$, with $DL$ differentiable at $\theta$. This states the regularity needed for the paper's Hessian notation explicitly, without requiring global smoothness or continuous second derivatives. A critical local minimum satisfies $DL(\theta)=0$ and has no smaller loss in some neighborhood; it may belong to a continuum of minima.

Symmetry, derivative transformation, and the goal theorem

The first milestone formalizes the scaling consequence of positive ReLU homogeneity in Theorem 1 and Definition 5, PDF p. 4:

$$f_{T_\alpha\theta}=f_\theta,\qquad L(T_\alpha\theta)=L(\theta),$$

and $T_\alpha\theta$ is a local minimum precisely when $\theta$ is. These statements hold for every parameter and every $\alpha>0$; the milestone itself requires no loss regularity.

The second milestone is Theorem 3, Section 4.2, PDF p. 5. At every point satisfying the stated local differentiability condition,

$$DL(T_\alpha\theta)[u]=DL(\theta)[T_{\alpha^{-1}}u],$$ $$H_L(T_\alpha\theta)[u,w] =H_L(\theta)[T_{\alpha^{-1}}u,T_{\alpha^{-1}}w]$$

for all parameter directions $u,w$. The same regularity holds at the rescaled point. This is the coordinate-free form of the paper's gradient formula and Hessian congruence with $D_\alpha=\operatorname{diag}(\alpha^{-1}I_{dh},\alpha I_h)$.

The goal is Theorem 4. If $\theta$ is a critical local minimum with the stated differentiability and $H_L(\theta)\ne0$, then

$$\forall M>0\ \exists\alpha>0:\qquad \|H_L(T_\alpha\theta)\|_2\ge M.$$

For that same rescaling, predictions and loss agree with the original ones, and the transformed parameter remains a critical local minimum with the required differentiability. The subscript $2$ denotes the Euclidean spectral norm. The source statement and its interpretation are in Section 4.2, PDF pp. 5–6. The relevant displays in all three targets are unnumbered.

What the formalization establishes

The result separates prediction behavior from this particular numerical measure of parameter-space curvature. Pointwise identical predictors have identical function-based evaluation losses wherever those are defined, even though their Hessian sharpness can be made arbitrarily large under the stated conditions. This is the scope of the obstruction: it concerns the unnormalized Euclidean Hessian norm and this rescaling symmetry. It does not assert that training reaches every point on a scaling orbit or supply a numerical bound on test error. Theorem 4 and following discussion, PDF p. 6.

The completed Lean development connects an explicitly computed ReLU prediction function to its actual first and second derivatives. It provides reusable results about invariant losses, transport of local minima, and curvature under linear changes of parameters. All three published theorem statements were proved unchanged and accepted on 26 September 2026. Both milestones are complete, and the goal has no remaining open leaves.

The analytic obligations

ReLU is not differentiable at every activation boundary. The loss-level local regularity must therefore be retained rather than inferred from the network's syntax. A nonzero symmetric matrix alone is also insufficient for the sharpness claim: local minimality supplies an additional sign constraint. Finally, the second derivative is an operator on the entire parameter space; bounds for a single arbitrarily chosen scalar model do not establish the quantified network result. These are obligations of the formal proof, not hypotheses assuming the desired transformation identities.

Formalization note: scope and conventions

Parameters are represented by EuclideanSpace over the disjoint union of first-layer matrix coordinates and output-weight coordinates. This retains the sum-of-squares geometry rather than a product maximum norm. The Hessian is the derivative of the actual Fréchet derivative, represented as a continuous bilinear form. Its operator norm is the spectral norm under the Euclidean/Riesz identification. The regularity condition excludes reliance on default derivative values at nondifferentiable points.

The statement covers every positive input dimension and hidden width, arbitrary function-based losses with the specified regularity, and arbitrary qualifying minima. It imposes no separate nonzero-weight or active-neuron assumption. An input or output weight block may vanish when the loss hypotheses still hold. The nonzero-Hessian requirement is essential. Scaling by zero or a negative number is outside the claim. No probability model, random initialization, sampling measure, or training algorithm is assumed.

The mission focuses on the single-hidden-layer Hessian result. Volume flatness, the multiple-eigenvalue deep-network theorem, and other reparameterizations remain separate results in the paper. The local environment is Lean 4.30.0 with supported Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f.

Selected references

• Laurent Dinh, Razvan Pascanu, Samy Bengio, Yoshua Bengio. Sharp Minima Can Generalize For Deep Nets. ICML 2017, PMLR 70:1019–1028. arXiv:1703.04933v2. Primary anchors: Section 2, PDF p. 2; Section 3, PDF pp. 3–4, Definitions 3–5 and Theorem 1; Section 4.2, PDF pp. 5–6, Theorems 3–4.
• Nitish Shirish Keskar, Dheevatsa Mudigere, Jorge Nocedal, Mikhail Smelyanskiy, Ping Tak Peter Tang. On Large-Batch Training for Deep Learning: Generalization Gap and Sharp Minima. ICLR 2017. arXiv:1609.04836v2. Historical context.

Why an initialization kernel matters

A neural network is nonlinear in its parameters, but a small change in those parameters changes its predictions through a Jacobian. The neural tangent kernel is the Gram kernel of that Jacobian: it records which changes in predictions can be produced by common parameter updates. An initialization limit identifies a deterministic object behind this random kernel. It supplies a mathematical starting point for studying wide networks through kernel methods, before addressing the additional question of how the kernel changes during training. Jacot, Gabriel, and Hongler establish this initialization limit in Section 4.1, Theorem 1, PDF p. 5.

The requested result is already a theorem of the paper. The open work here is its formal proof in Lean, including the probability model and the order of limits. The mission is classified as OpenProblem at the request of its proposer; that label does not assert that the underlying mathematical result remains an unsolved research question.

The source appeared in 2018 and was published at NeurIPS 2018; this formalization fixes arXiv version 4, dated February 10, 2020, so that page references and conventions remain stable. Its Appendix A explicitly distinguishes the sequential limit proved there from a possible stronger simultaneous-width limit.

Networks, randomness, and the two kernels

Fix positive integers $d$ and $q$, the input and output dimensions, a hidden-layer count $h\ge0$, a bias scale $\beta>0$, and a Lipschitz function $\sigma:\mathbb R\to\mathbb R$. Write $L=h+1$ for the number of affine layers, with $n_0=d$, $n_L=q$, and positive hidden widths $n_1,\ldots,n_h$. The parameters are all entries of the weight matrices and bias vectors. Every parameter is sampled independently from $\mathcal N(0,1)$.

For an input $x$, let $a^{(0)}(x)=x$ and define

$$z^{(\ell+1)}_j(x)=\frac1{\sqrt{n_\ell}} \sum_i W^{(\ell)}_{ji}a^{(\ell)}_i(x)+\beta b^{(\ell)}_j.$$

At each hidden layer, $a^{(\ell)}=\sigma(z^{(\ell)})$ coordinatewise. The output is $f_\theta(x)=z^{(L)}(x)$, with no final activation. These are the conventions of Section 2, PDF pp. 2–3. Matrix storage order in Lean uses destination then source; the displayed operation is unchanged.

For output coordinates $k,k'$, set

$$\Theta^{(L)}_{kk'}(\theta;x,y)=\sum_p \partial_{\theta_p}f_{\theta,k}(x)\, \partial_{\theta_p}f_{\theta,k'}(y).$$

The sum includes every weight and every bias, as in Section 4, PDF p. 5.

The covariance kernel starts with

$$\Sigma^{(1)}(x,y)=\frac{\langle x,y\rangle}{d}+\beta^2.$$

Given a centered Gaussian pair $(U,V)$ with covariance matrix obtained by evaluating $\Sigma^{(\ell)}$ on $(x,y)$, define

$$\Sigma^{(\ell+1)}(x,y)=\mathbb E[\sigma(U)\sigma(V)]+\beta^2, \qquad \dot\Sigma^{(\ell+1)}(x,y)=\mathbb E[\sigma'(U)\sigma'(V)].$$

The deterministic limiting NTK is

$$\Theta_\infty^{(1)}=\Sigma^{(1)},\qquad \Theta_\infty^{(\ell+1)}(x,y)=\Theta_\infty^{(\ell)}(x,y) \dot\Sigma^{(\ell+1)}(x,y)+\Sigma^{(\ell+1)}(x,y).$$

These recurrences appear in Section 4.1, Proposition 1 and Theorem 1, PDF p. 5; their displays are unnumbered.

Formalization targets

The goal is Theorem 1, on every fixed finite family $X=(x_1,\ldots,x_N)$ of inputs and for every $\varepsilon>0$:

$$\Pr\!\left(\exists i,j,k,k': \left|\Theta^{(L)}_{kk'}(\theta;x_i,x_j) -\Theta_\infty^{(L)}(x_i,x_j)\delta_{kk'}\right|>\varepsilon\right) \longrightarrow0.$$

Here $\delta_{kk'}$ is one when the output coordinates coincide and zero otherwise. The limit takes $n_1\to\infty$ first, then $n_2\to\infty$, through $n_h\to\infty$, precisely as specified in Appendix A, PDF p. 11, and Appendix A.1, PDF pp. 12–13.

Two supporting milestones expose the required mathematical content. First, the recursively defined $\Sigma^{(L)}$ has positive semidefinite Gram matrices on every finite input family and satisfies $\Sigma^{(L)}(x,x)\ge\beta^2$. This is a paper-derived well-definedness obligation for the covariance in Proposition 1. Second, Proposition 1 asserts joint convergence in distribution of $(f_{\theta,k}(x_i))_{i,k}$ to the centered Gaussian vector with covariance $\Sigma^{(L)}(x_i,x_j)\delta_{kk'}$. This expresses the paper's independent output Gaussian processes through all their finite-dimensional distributions.

What completing the mission would establish

The result connects an explicitly parameterized random finite network to a deterministic kernel computed from its activation and depth. All output correlations, bias contributions, and layer normalizations remain visible in that connection. It would provide a checked foundation on which a separate training-stability development could build.

The formal contribution is the passage from finite random Jacobians to the limiting kernel. It does not assume that the empirical NTK already equals its limit. Nor does the goal claim convergence of a training trajectory, positive definiteness on a sphere, an early-stopping guarantee, or a generalization bound; those are separate results and questions in the source.

Where the mathematical work lies

The parameter space changes with the widths. Outputs, hidden activations, and their parameter derivatives are dependent random quantities, so the limit of their products requires more than a scalar law of large numbers. The weak Gaussian limit alone also does not justify substituting an arbitrary discontinuous derivative into expectations. The Lipschitz-only hypothesis is part of the target and must be retained, including for nonsmooth activations. Remark 3, PDF p. 5 identifies almost-everywhere differentiation as the relevant convention.

Formalization scope and conventions

Lean represents parameter coordinates by a finite dependent index carrying a layer, destination neuron, and optional source neuron; the missing source denotes a bias. Initialization is the finite product of Mathlib's standard Gaussian measures. Network outputs are obtained by the displayed recursion, and NTK entries use actual Fréchet derivatives in coordinate directions. Mathlib's derivative is zero where differentiation fails; the proof must establish that the exceptional parameters are null under the stated initialization law.

Centered Gaussian laws use Mathlib's multivariateGaussian, including singular covariance. The covariance-validity milestone must justify its covariance interpretation. No invertibility, distinct-input, smooth-activation, or positive-definite-kernel assumption is added. Positive actual hidden widths are indexed as $w_i+1$ for $w_i\in\mathbb N$, a cofinal reindexing. Depth one, constant activations, repeated or zero inputs, and empty finite families are included. The empty family is harmless because the same theorem quantifies over every nonempty family as well.

The sequential filter puts the last hidden width outermost. For two hidden widths, a probability tolerance is met by first choosing a threshold for $n_2$, then a threshold for $n_1$ that may depend on $n_2$. There is no uniform limit over the entire input space and no simultaneous-width assertion. The development uses Lean 4.30.0 and supported Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. The model and statements are locally checked; the three theorem proofs remain open. Contributions to Gaussian covariance consistency, finite-dimensional distribution limits, almost-everywhere network differentiation, and the NTK limit are in scope.

Selected references

• Arthur Jacot, Franck Gabriel, and Clément Hongler, Neural Tangent Kernel: Convergence and Generalization in Neural Networks, Advances in Neural Information Processing Systems 31, 2018. arXiv:1806.07572v4. Primary anchors: Section 2, PDF pp. 2–3; Section 4.1, PDF p. 5, Proposition 1, Theorem 1, Remarks 2–3; Appendix A and A.1, PDF pp. 11–13. Relevant displays have no equation numbers.

Why stochastic-gradient convergence matters

Training a machine-learning model often means choosing a vector of parameters to minimize an average loss. Evaluating the full gradient can require processing an entire dataset. A stochastic-gradient method instead updates the parameters using a random direction obtained from a smaller amount of information. Its computational appeal raises a mathematical question: which assumptions on those directions and the stepsizes guarantee progress, and what kind of convergence follows?

This mission formalizes the core convergence theory in Section 4 of Bottou, Curtis, and Nocedal, Optimization Methods for Large-Scale Machine Learning. The results distinguish strongly convex objectives, where expected objective error can be controlled, from general smooth objectives, where the guarantee concerns gradients. They also distinguish constant stepsizes, which leave a noise-dependent error bound, from diminishing stepsizes.

Historical timeline

• 1951: Robbins and Monro introduced stochastic approximation for finding a root using noisy observations. Their work is the historical foundation for the stepsize conditions used here; the original root-finding theorem is not a separate target of this mission. Original paper.
• 2016: Bottou, Curtis, and Nocedal released the first version of their survey, organizing stochastic-gradient theory around smoothness and moment assumptions. arXiv record.
• 2018: The revised survey appeared in SIAM Review. This mission fixes arXiv version 3 for stable theorem numbering and PDF page citations. Published article.

The mathematics targeted here is already proved in the literature; the task is its Lean formalization, not a claim that these convergence results are unresolved research conjectures.

Objective, algorithm, and probability model

Let $F:\mathbb R^d\to\mathbb R$ be differentiable with an $L$-Lipschitz gradient, where $L>0$. On a probability space $(\Omega,\mathcal A,\mathbb P)$, let $\mathcal H_k$ contain the history before step $k$. Starting from a deterministic vector $w_0$, the algorithm uses positive deterministic stepsizes $\alpha_k$ and random directions $g_k$ to update

$$w_{k+1}=w_k-\alpha_k g_k.$$

The state $w_k$ is measurable with respect to $\mathcal H_k$; the direction $g_k$ is measurable with respect to $\mathcal H_{k+1}$ and has a finite second moment. Conditional assertions hold almost surely. This uses the adapted-process formulation expressly permitted in footnote 4, PDF p. 22, rather than requiring independent sample seeds. The local index $k=0$ corresponds to the paper's $k=1$. Algorithm 4.1 and footnote 4.

Write $\mathbb E_k$ for conditioning on $\mathcal H_k$. The moment conditions use constants $\mu_G\ge\mu>0$ and $M,M_V\ge0$:

$$\langle\nabla F(w_k),\mathbb E_k g_k\rangle\ge\mu\|\nabla F(w_k)\|^2, \qquad \|\mathbb E_k g_k\|\le\mu_G\|\nabla F(w_k)\|,$$ $$\mathbb E_k\|g_k\|^2-\|\mathbb E_k g_k\|^2 \le M+M_V\|\nabla F(w_k)\|^2.$$

Define $M_G=M_V+\mu_G^2$. The iterates lie almost surely in an open region on which $F\ge F_{\inf}$ for a real lower bound $F_{\inf}$. These are Assumptions 4.1 and 4.3, PDF pp. 23–24, equations (4.6)–(4.9). Source.

Formalization targets

The goal is Theorem 4.10, Section 4.3, PDF p. 33, equations (4.30a)–(4.30b). Suppose

$$\sum_{k=0}^\infty\alpha_k=\infty,\qquad \sum_{k=0}^\infty\alpha_k^2<\infty.$$

For $A_K=\sum_{k=0}^{K-1}\alpha_k$, establish both

$$\exists S\in\mathbb R:\quad \mathbb E\!\left[\sum_{k=0}^{K-1}\alpha_k\|\nabla F(w_k)\|^2\right]\longrightarrow S,$$ $$\frac{1}{A_K}\mathbb E\!\left[\sum_{k=0}^{K-1}\alpha_k\|\nabla F(w_k)\|^2\right] \longrightarrow0.$$

There is no convexity assumption and no restriction that the initial stepsizes already satisfy a small-step bound. Theorem 4.10.

Four milestones capture the surrounding theory. Lemma 4.4 gives the two successive conditional expected-descent inequalities (4.10a)–(4.10b), PDF pp. 24–25. It is a common input to the convergence results. Theorem 4.6 gives a geometric upper bound for strongly convex objectives with a constant stepsize. Theorem 4.7 gives the corresponding $O(1/k)$ bound for $\alpha_k=\beta/(\gamma+k+1)$. These are parallel strongly convex targets, not prerequisites for the nonconvex goal. Theorem 4.8 gives finite-horizon sum and average squared-gradient bounds for general objectives with a constant stepsize. Section 4.

For example, if $c>0$ is the strong-convexity constant, $d\ge1$, and $0<a\le\mu/(LM_G)$, Theorem 4.6 states, with $B=aLM/(2c\mu)$ and $F_*=\inf_xF(x)$,

$$\mathbb E[F(w_k)-F_*]\le B+(1-ac\mu)^k(F(w_0)-F_*-B).$$

The upper bound tends to $B$; this does not assert that the actual expected error tends to $B$. Every milestone retains the paper's constants and all displayed conclusions. Equations (4.13)–(4.14), PDF p. 26.

What a completed formalization provides

The result explains precisely how noise and stepsize interact. The general-objective goal guarantees that the stepsize-weighted expected squared gradients average to zero even when $M>0$. The strongly convex milestones quantify objective error and the effect of initialization. These results concern the stated quantities; they do not assert convergence of iterates, global optimality for a nonconvex objective, or almost-sure convergence. Sections 4.2–4.3.

A completed development would provide reusable Lean results for smooth objective functions, conditional moment bounds, stochastic updates, and expected convergence. The proposed statements are open proof obligations. Compilation establishes that the definitions and statements are well formed, not that their convergence claims have already been proved.

Mathematical and formal difficulties

Finite conditional expectations must be connected to unconditional integrals without relying on total-function defaults. The infinite-horizon result also requires careful handling of a finite initial segment: square summability gives eventually small steps, not a bound at every step. Strong convexity must justify the objective-gap estimates and the properties of the optimum. Treating a descent recurrence as a hypothesis would omit the analytic content that this mission is intended to formalize.

Formalization scope

The model uses real finite-dimensional Euclidean space, Mathlib gradients, filtrations, Bochner conditional expectations, and ordinary real integrals. The probability space is arbitrary; no finite-support or standard-Borel restriction is imposed. Directions have explicit finite second moments, making the finite-expectation convention in the paper visible. Square integrability of iterates and integrability of losses are consequences to establish, not extra model fields.

Strong convexity uses Mathlib's StrongConvexOn, equivalent here to Assumption 4.5's first-order inequality. The optimum is defined as the infimum of the range of $F$, with its finiteness to be derived in the strongly convex branch. That branch requires $d\ge1$: the paper's deduction $c\le L$ implicitly uses a nontrivial space. The nonconvex statements allow $d=0$. Zero noise is allowed. Finite-horizon averages require $K>0$; the value assigned at $K=0$ does not affect an asymptotic limit.

Contributions to the conditional-descent infrastructure and any of the four milestones are welcome. Variance reduction, Newton-type methods, and the remainder of the survey are outside this initial mission.

Selected references

• Léon Bottou, Frank E. Curtis, and Jorge Nocedal. Optimization Methods for Large-Scale Machine Learning. SIAM Review 60(2), 223–311, 2018. arXiv:1606.04838v3; DOI. All page numbers above refer to the 95-page arXiv v3 PDF.
• Herbert Robbins and Sutton Monro. A Stochastic Approximation Method. Annals of Mathematical Statistics 22(3), 400–407, 1951. DOI. Historical background only.

Why control variates matter in federated optimization

Federated optimization trains one model using objectives held by many clients. Performing several local updates between communication rounds saves communication, but clients with different objectives can move in different directions. SCAFFOLD maintains a correction for each client to address this disagreement, including when only some clients participate. Karimireddy et al. establish convergence without a bound on how similar the client objectives are. The relevant result is Theorem III, Section 5, PDF p. 5.

SCAFFOLD: Convergence with Client Sampling concerns that known result's formalization. Its exact targets are finite-round bounds from the Appendix E analysis, covering strongly convex, general convex, and nonconvex objectives. The paper's FedAvg results and its separate quadratic-acceleration theorem are outside this scope.

Setting: local updates and sampled clients

There are $N\ge1$ clients, with differentiable objectives $f_i:\mathbb R^d\to\mathbb R$. The global objective is $f(x)=N^{-1}\sum_i f_i(x)$. Every client gradient is $\beta$-Lipschitz, where $\beta>0$. A stochastic gradient query is conditionally unbiased and has conditional squared-error expectation at most $\sigma^2$, with $\sigma\ge0$. Current queries on different clients are conditionally independent given the full history. These make precise the fresh-oracle interpretation of A4–A5, Appendix B.1, PDF p. 14.

Each of $T\ge1$ rounds selects a uniform subset $A_r$ of $S$ clients, where $1\le S\le N$. Each selected client takes $K\ge1$ local steps. Let $x^r$ be the server model, $c_i^r$ its stored client control variates, and $c^r=N^{-1}\sum_i c_i^r$. With constant local and global step sizes $\eta_l>0$ and $\eta_g\ge1$, a client starts at $y_{i,0}^r=x^r$ and uses

$$y_{i,k+1}^r=y_{i,k}^r-\eta_l\bigl(g_{i,k}^r-c_i^r+c^r\bigr), \qquad x^{r+1}=x^r+\frac{\eta_g}{S}\sum_{i\in A_r}(y_{i,K}^r-x^r).$$

Option II replaces a participating client's control with $K^{-1}\sum_{k=0}^{K-1}g_{i,k}^r$ and retains every other control. These are Algorithm 1, PDF p. 4, and Appendix E, equations (18)–(21), PDF pp. 25–26. Write $h=K\eta_l\eta_g$ for the effective step size.

Formalization targets

Four milestones support a root goal that is the conjunction of the two convergence statements below.

GradientGrowth states, for convex clients and a global minimizer $x^\star$,

$$\frac1N\sum_i\|\nabla f_i(x)-\nabla f_i(x^\star)\|^2 \le2\beta\bigl(f(x)-f(x^\star)\bigr).$$

This is Appendix B.1, equation (9), PDF p. 14. PerturbedStrongConvexity states, for each $\mu$-strongly convex client and $\mu\ge0$,

$$\langle\nabla f_i(x),z-y\rangle\ge f_i(z)-f_i(y) +\frac\mu4\|y-z\|^2-\beta\|z-x\|^2,$$

as in Appendix C, Lemma 5, PDF p. 17.

ConvexFiniteRoundConvergence allows arbitrary deterministic initial controls $c_i^0$. Assume all clients are $\mu$-strongly convex with $\mu\ge0$, including ordinary convexity when $\mu=0$, and fix a minimizer $x^\star$ of $f$. Define

$$C_0=\frac1N\sum_i\|c_i^0-\nabla f_i(x^\star)\|^2, \qquad V_0=\|x^0-x^\star\|^2+\frac{9Nh^2}{S}C_0,$$ $$q=1-\frac{\mu h}{2},\qquad w_r=q^{-(r+1)},\qquad W_T=\sum_{r=0}^{T-1}w_r.$$

For $h\le1/(81\beta)$ and $\mu h\le S/(15N)$, the target is

$$\frac1{W_T}\sum_{r=0}^{T-1}w_r\, \mathbb E\bigl[f(x^r)-f(x^\star)\bigr] \le\frac{V_0}{hW_T} +\frac{12h\sigma^2}{KS}\left(1+\frac S{\eta_g^2}\right).$$

This is a finite-round formulation of Appendix E.1, Lemma 15, PDF p. 30; its $\mu=0$ case is the first bound on PDF p. 31.

NonconvexFiniteRoundConvergence assumes a lower bound $f_\mathrm{lower}$ for $f$ and initializes every client control with $K$ fresh gradients at $x^0$. Put $F_0=f(x^0)-f_\mathrm{lower}$. For $h\le(S/N)^{2/3}/(24\beta)$, establish

$$\frac1T\sum_{r=0}^{T-1}\mathbb E\|\nabla f(x^r)\|^2 \le\frac{14F_0}{hT} +\frac{70\beta h\sigma^2}{KS}\left(1+\frac S{\eta_g^2}\right).$$

This is the explicit finite-round consequence targeted from Appendix E.2, Lemma 19, PDF p. 34, with the initialization specified on PDF pp. 31 and 35. The full-client warm start's communication cost is separate from these $T$ optimization rounds.

What the result establishes

The bounds quantify optimization progress under stochastic gradients, several local steps, and partial participation. They permit arbitrarily different client objectives within the stated smoothness and convexity assumptions. Their output is a weighted random server iterate, represented by its expected loss, or a uniform random server iterate for the squared-gradient guarantee; this follows the output convention in equation (22), PDF p. 26.

The mathematical convergence analysis is published. The open work here is a Lean proof under the explicit stochastic-run model. The proposed statements do not themselves supply a machine-checked convergence proof. A completed development would provide reusable results about sampled finite averages, adaptive gradient queries, and optimization with stored noisy controls.

Where the difficulty lies

Local gradients are evaluated at different client states, and inactive clients retain controls computed in earlier rounds. Consequently, treating the server update as a centralized stochastic-gradient step discards both local disagreement and stale-control error. The challenge is to control these quantities while preserving their dependence on earlier randomness, as reflected in Appendix E.1–E.2, PDF pp. 26–35.

The source also needs careful transcription. The printed Theorem VII nonconvex noise term on PDF p. 25 differs from Lemma 19 in its smoothness and sampling factors, while output indices differ between equation (22) and the finite sum on p. 31. The exact targets above use the proof's finite-round constants and explicit indexing; they do not claim a verbatim formalization of every printed asymptotic rate.

Formalization scope

SCAFFOLD.Space is finite-dimensional real Euclidean space; SCAFFOLD.Problem records differentiable client objectives and smoothness. SCAFFOLD.Run records a standard Borel probability space, full-history filtration, measurable square-integrable iterates and oracle samples, and the concrete updates. Virtual local paths are generated before a fresh uniform size-$S$ subset is sampled, as permitted by the paragraph after equation (22), PDF p. 26.

The conventions include $S=N$, $K=1$, zero noise, and $\mu=0$. The output indices are precisely $0,\ldots,T-1$. Convex initial controls are deterministic; the nonconvex branch uses the specified stochastic warm start. The run definition assumes no descent inequality or convergence conclusion. Contributions should establish the four named propositions and necessary analysis/probability infrastructure while retaining these semantics.

Selected references

• Sai Praneeth Karimireddy, Satyen Kale, Mehryar Mohri, Sashank J. Reddi, Sebastian U. Stich, and Ananda Theertha Suresh, SCAFFOLD: Stochastic Controlled Averaging for Federated Learning, ICML 2020, PMLR 119:5132–5143; arXiv:1910.06378v4, revised 2021. Primary scope: Theorem III, PDF p. 5; A3–A5 and (9), p. 14; Lemma 5, p. 17; Appendix E, pp. 25–35, especially Lemmas 15 and 19.

Why local training needs a convergence guarantee

Federated optimization studies learning when data and computation are spread across clients. Communicating after every stochastic gradient step can be costly, so clients often take several steps before averaging their models. The difficulty is that different clients can optimize different objective functions. Their models then move apart between communication rounds. A convergence guarantee must account for both stochastic gradient noise and this disagreement. Wang et al. give an explicit analysis of this tradeoff in A Field Guide to Federated Optimization, Section 6.1.

The relevant historical sequence is the introduction of FedAvg by McMahan et al. in 2017, the development of local-SGD convergence analyses reviewed by Wang et al., and the unified illustrative analysis in the 2021 field guide. The present target is that guide's known convex convergence theorem, rather than a new conjecture about arbitrary federated learning. The remaining open task is a Lean proof of the stated result. The mission is categorized as ResearchPaper: it formalizes a specific known result rather than proposing a new mathematical conjecture.

Setting: full participation with uniform weights

There are $M\ge1$ clients and a parameter vector in $\mathbb R^d$. Client $i$ has a differentiable convex objective $F_i$. The global objective is $F(x)=M^{-1}\sum_{i=1}^M F_i(x)$. Every local gradient is $L$-Lipschitz for the same $L>0$. Fix a global minimizer $x^\star$ of $F$ and a deterministic initial model $x_0$, and write $D=\|x_0-x^\star\|$.

Every client participates in every round. Each of $T\ge1$ rounds consists of $\tau\ge1$ local steps with constant learning rate $\eta$. If $x_i^{t,k}$ is client $i$'s state after $k$ local steps of round $t$, its next state is $x_i^{t,k+1}=x_i^{t,k}-\eta g_i^{t,k}$. At the next round all clients restart from the average of the preceding round's terminal states. The shadow iterate is $\bar x^{t,k}=M^{-1}\sum_i x_i^{t,k}$; it is defined even at local steps where clients do not communicate.

On a probability space $(\Omega,\mathcal A,\mathbb P)$, the history before a step contains all past oracle draws. The stochastic gradients are conditionally unbiased, their conditional squared errors have expectation at most $\sigma^2$, and the different clients' current gradients are conditionally independent. The heterogeneity bound is $\|\nabla F_i(x)-\nabla F(x)\|\le\zeta$ for every client and every point, where $\sigma,\zeta\ge0$. These are the assumptions of Section 6.1.1, PDF p. 40, equations (11)–(14), with the history and independence convention used explicitly in Appendix D.1 immediately after equation (27), PDF p. 87.

Formalization targets

The principal goal is Theorem 1, equation (15). For $0<\eta\le1/(4L)$, establish

$$\mathbb E\!\left[\frac1{\tau T}\sum_{t=0}^{T-1}\sum_{k=1}^{\tau} \bigl(F(\bar x^{t,k})-F(x^\star)\bigr)\right] \le \frac{D^2}{2\eta\tau T}+\frac{\eta\sigma^2}{M} +4\tau\eta^2L\sigma^2+18\tau^2\eta^2L\zeta^2.$$

Two source milestones describe the intermediate results. Lemma 1 bounds the conditional average loss within a round by the decrease of squared distance to the minimizer, plus a noise term and a sum of client disagreements. Lemma 2 bounds each conditional squared disagreement by $18\tau^2\eta^2\zeta^2+4\tau\eta^2\sigma^2$. Both are stated on PDF p. 41, Section 6.1.2, with proofs in Appendix D, PDF pp. 86–88. They remain genuine open proof obligations; the algorithm model does not assume either estimate.

An additional milestone records the same theorem's tuned-step consequence, equations (16)–(17), in the regime $D,\sigma,\zeta>0$. With

$$\eta=\min\left\{\frac1{4L}, \frac{\sqrt M D}{\sqrt\tau\sqrt T\sigma}, \frac{D^{2/3}}{\tau^{2/3}T^{1/3}L^{1/3}\sigma^{2/3}}, \frac{D^{2/3}}{\tau T^{1/3}L^{1/3}\zeta^{2/3}}\right\},$$

the same expected loss is at most

$$\frac{2LD^2}{\tau T}+\frac{2\sigma D}{\sqrt{M\tau T}} +\frac{5L^{1/3}\sigma^{2/3}D^{4/3}}{\tau^{1/3}T^{2/3}} +\frac{19L^{1/3}\zeta^{2/3}D^{4/3}}{T^{2/3}}.$$

The principal goal includes zero-noise and zero-heterogeneity cases. The extra positivity conditions apply only to the printed tuned-step formula, whose denominators otherwise require separate conventions.

What this establishes

The bound separates an initial-distance term, a noise term improved by the number of clients, and two costs of local updates. It quantifies how local work interacts with stochastic noise and differing client objectives. Its conclusion concerns the average objective gap along the post-update shadow sequence; it does not assert the same bound for every last iterate or for the average of client losses. These distinctions follow directly from the quantity defined in equation (14).

A completed formalization would provide reusable checked components for stochastic optimization: finite client averages, history-conditioned oracle assumptions, per-round potential estimates, and disagreement bounds. The paper supplies the mathematical proof; this draft supplies checked statements and definitions. No convergence proof is claimed by creating or compiling the proposal.

Where the difficulty lies

The average update evaluates each gradient at its own client's state. It therefore does not directly equal a centralized stochastic-gradient step at the shadow iterate. A proof must control that discrepancy quantitatively, preserve the conditioning on the round's starting history, and justify the $1/M$ noise improvement using independent client sampling. Ignoring the sampling relationship can invalidate the advertised bound even for scalar quadratic objectives.

Formalization scope

The model uses finite-dimensional real Euclidean space, including the harmless zero-dimensional case, and a standard Borel probability space. A filtration indexed by $t\tau+k$ records the full past. Local states and gradients carry explicit measurability and finite-second-moment conditions. These probability conventions support actual Bochner and conditional expectations; integrals are not treated as arbitrary total functions without analytic obligations.

The local objectives, global objective, gradients, iterates, and shadow averages are concrete functions. The model assumes neither a drift bound nor a progress bound. Source hypotheses are uniform in the model point, and the minimizer is an actual minimizer of the averaged objective. Unequal weighting, partial client participation, nonconvex objectives, adaptive step sizes, and privacy mechanisms are outside this particular theorem. Contributions should prove the named source lemmas or their necessary analytic infrastructure while retaining these statements.

Selected references

• Jianyu Wang et al., A Field Guide to Federated Optimization, 2021, arXiv:2107.06917v1, Section 6.1.1–6.1.2, PDF pp. 40–41; Appendix D, PDF pp. 86–88.
• H. Brendan McMahan et al., Communication-Efficient Learning of Deep Networks from Decentralized Data, AISTATS 2017, arXiv:1602.05629, the FedAvg algorithm cited by the field guide. This is historical context, not an additional target.