01
Introduction and basics of convex functions
§1 · 11 mapped, independently verified local proof declarations. Source equivalence and chapter completion are separate.
Optimisation Library · Sinho Chewi
Lectures on Optimization
A public theorem-proof formalization route following arXiv:2605.07006 section by section.
Source hierarchy
Chewi is the formalization target; Beck is background.
Chewi's notes are the controlling public source. The notes themselves state that they are primarily based on Bubeck (2015), Beck (2017), and Nesterov (2018). Those works remain attributed background and cross-check references. Mathlib, Optlib, and CvxLean are searched before new Lean declarations are introduced.
reuseadaptmissingout of scope
Lecture-note contents
13 chapters + Appendix A
02
Gradient flow
§2 · 6 mapped, independently verified local proof declarations. Source equivalence and chapter completion are separate.
03
Gradient descent: smooth case
§3 · 20 mapped, independently verified local proof declarations. Source equivalence and chapter completion are separate.
04
Lower bounds for smooth optimization
§4 · 6 mapped, independently verified local proof declarations. Source equivalence and chapter completion are separate.
05
Acceleration
§5 · 0 mapped, independently verified local proof declarations. Source equivalence and chapter completion are separate.
06
Non-smooth convex optimization
§6 · 0 mapped, independently verified local proof declarations. Source equivalence and chapter completion are separate.
07
Frank-Wolfe
§7 · 0 mapped, independently verified local proof declarations. Source equivalence and chapter completion are separate.
08
Proximal methods
§8 · 0 mapped, independently verified local proof declarations. Source equivalence and chapter completion are separate.
09
Fenchel duality
§9 · 0 mapped, independently verified local proof declarations. Source equivalence and chapter completion are separate.
10
Mirror methods
§10 · 0 mapped, independently verified local proof declarations. Source equivalence and chapter completion are separate.
11
Alternating minimization
§11 · 0 mapped, independently verified local proof declarations. Source equivalence and chapter completion are separate.
12
Stochastic optimization
§12 · 0 mapped, independently verified local proof declarations. Source equivalence and chapter completion are separate.
13
Interior point methods
§13 · 0 mapped, independently verified local proof declarations. Source equivalence and chapter completion are separate.
A
Background on symmetric matrices
Appendix A · 0 mapped, independently verified local proof declarations. Source equivalence and chapter completion are separate.
Formal upstreams
Reuse checked formal mathematics before reproving it.
Optlib
Convex analysis, proximal maps, first-order algorithms, acceleration, block methods, and ADMM.
Open Optlib ↗CvxLean
Formal optimization problems, equivalence, reduction, relaxation, and verified transformations.
Open CvxLean ↗