Samplinglib
Lean gate not recorded for this source state main · ed709a7f320d

Samplinglib · research resources

Optlib: mathematical reuse map

Browse an external library by purpose; inspect source-backed local mathematics without confusing provenance with a compiled dependency.

Optlib uses leanprover/lean4:v4.13.0. Samplinglib stays on Lean 4.33.0 and its fixed Mathlib. No new Optlib dependency or bulk port was added.

Native Samplinglib results

Explicit primary-source bindings, not inferred citations. These nodes use our pinned compiler and existing definitions; each reader contains the formula proof and adjacent optional Lean. This is not a bulk-port or chapter-completion claim.

Five mathematical areas

Differential calculus

Gradients, chain/product rules, mean-value and Taylor arguments.

Related source chapter (reading context only)

Shared analytic floor for Euclidean energy estimates. Riemannian gradients require their own tangent-space and metric adapter.

Browse 5 upstream modules

Convex analysis

Convexity, strong convexity, subgradients, cones and separation.

Related source chapter (reading context only)

Potential curvature can feed log-concavity prerequisites. It does not by itself prove a functional inequality, mixing bound or invariant law.

Browse 11 upstream modules

Smoothness and proximal structure

Smoothness models, lower semicontinuity, proximal maps and Kurdyka–Łojasiewicz structure.

Related source chapter (reading context only)

A proximal minimizer and a Gibbs/RGO draw are different objects. Also distinguish Kurdyka–Łojasiewicz properties from Kullback–Leibler divergence.

Browse 6 upstream modules

Optimality and duality

Unconstrained stationarity, constraint qualifications, KKT and weak duality.

Related source chapter (reading context only)

Transport and constrained algorithms need their own primal/dual spaces, attainment and constraint qualifications; do not infer them from an analogy.

Browse 4 upstream modules

Algorithms and complexity

Gradient/subgradient methods, proximal gradient, acceleration, LASSO, BCD and ADMM.

Related source chapter (reading context only)

Compare actual updates, potential estimates and oracle models. No optimization convergence theorem is silently promoted into sampling complexity.

Browse 15 upstream modules

Existing local proof readers citing Optlib

Generated from canonical authored lessons, not a second port-status table. A citation is not necessarily a code port or imported dependency. Each linked reader shows its actual statement, proof, folded Lean and review boundary.

Tools, publications and textbooks indexed by Optlib

Code Explanations

  1. Basic.lean external reference
  2. Strong.lean (upstream migration reference) external reference
  3. ClosedFunction.lean external reference

Topics

  1. Convex Analysis (R. T. Rockafellar) external reference
  2. Numerical Optimization (Jorge Nocedal, Stephen J. Wright) external reference
  3. Optimization: Modeling, Algorithm and Theory external reference
  4. Integer Programming (Michele Conforti, Gérard Cornuéjols, and Giacomo Zambelli) external reference
  5. Matrix Computations (Golub & Van Loan) external reference
  6. High-Dimensional Probability (Roman Vershynin) external reference

Lean Projects

  1. ReasLab external reference
  2. Optlib external reference
  3. ReasBook external reference
  4. AMBER external reference
  5. M2F external reference
  6. SITA external reference
  7. lean-tools-mcp external reference

Publications

  1. Wanli Ma, Zichen Wang, Zaiwen Wen, *A Unified Framework for Formalizing Matrix Decomposition Proofs*. external reference
  2. Chenyi Li, Ziyu Wang, Wanyi He, Yuxuan Wu, Shengyang Xu, Zaiwen Wen. Formalization of Complexity Analysis of the First-order Optimization Algorithms, Journal of Automated Reasoning external reference
  3. Chenyi Li, Zichen Wang, Yifan Bai, Yunxi Duan, Yuqing Gao, Pengfei Hao, Zaiwen Wen, Formalization of Algorithms for Optimization with Block Structures, Science in China Series A: Mathematics external reference
  4. Chenyi Li, Shengyang Xu, Chumin Sun, Li Zhou, Zaiwen Wen, Formalization of Optimality Conditions for Smooth Constrained Optimization Problems external reference
  5. Chenyi Li, Zaiwen Wen, An Introduction to Mathematics Formalization Based on Lean (in Chinese external reference
  6. Ziyu Wang, Bowen Yang, Chenyi Li, Yuan Zhang, Shihao Zhou, Bin Dong, Zaiwen Wen, Translating Informal Proofs into Formal Proofs Using a Chain of States external reference
  7. Chenyi Li, Wanli Ma, Zichen Wang, Zaiwen Wen, SITA: A Framework for Structure-to-Instance Theorem Autoformalization, AAAI, 2026 external reference
  8. Chenyi Li, Yanchen Nie, Zhenyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen, OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving external referenceUpstream lists this title without a paper URL; link opens its README citation, not an inferred manuscript.
  9. Zichen Wang, Wanli Ma, Zhenyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen, M2F: Automated Formalization of Mathematical Literature at Scale external reference
  10. Zichen Wang, Anjie Dong, Zaiwen Wen, Tree-Based Premise Selection for Lean4, Nips, 2025 external reference
  11. Shu Miao, Zichen Wang, Anjie Dong, Yishan Wu, Weixi Zhang, Zaiwen Wen, Directed Multi-Relational GCNs for Premise Selection external referenceUpstream lists this title without a paper URL; link opens its README citation, not an inferred manuscript.
  12. Bowen Yang, Yi Yuan, Chenyi Li, Ziyu Wang, Liangqi Li, Bo Zhang, Zhe Li, Zaiwen Wen, Construction–Verification: A Benchmark for Formalizing Applied Mathematics in Lean 4 external reference

References

  1. H. Liu, J. Hu, Y. Li, Z. Wen, Optimization: Modeling, Algorithm and Theory (in Chinese) external reference
  2. Rockafellar, R. Tyrrell, and Roger J-B. Wets. Variational analysis. Vol. 317. Springer Science & Business Media, 2009. external reference
  3. Nocedal, Jorge, and Stephen J. Wright, eds. Numerical optimization. New York, NY: Springer New York, 1999. external reference
  4. Nesterov, Yurii. Lectures on convex optimization. Vol. 137. Berlin: Springer, 2018. external reference
  5. Convex Analysis, Vol. 28 of Princeton Math. Series, Princeton Univ. Press, 1970 external reference
  6. Bolte, J., Sabach, S. & Teboulle, M. Proximal alternating linearized minimization for nonconvex and nonsmooth problems. Math. Program. 146, 459–494 (2014). external reference
  7. Maryam Fazel, Ting Kei Pong, Defeng Sun, and Paul Tseng. Hankel matrix rank minimization with applications to system identification and realization. SIAM Journal on Matrix Analysis and Applications, 34(3):946–977, 2013 external reference
Reuse checklist and upstream link caveats
  1. Search our declaration catalog, fixed Mathlib, active shared cells, then this pinned upstream.
  2. Read the exact definition, quantifiers, positivity and regularity assumptions; inspect placeholders and axioms before any port.
  3. Choose reuse, an explicit adapter, a genuine missing shared leaf, or out of scope. Record real consumers.
  4. Compile an owned declaration, test it, complete independent source review and publish the readable formula proof through the existing protocol.

The upstream README contains stale Function/BanachSubgradient and Function/FiniteDimensionalConvexFunctionsLocallyLipschitz paths and a doubled slash in an acceleration link. The complete module list above uses the pinned Git tree, not those broken paths. Mathlib pointers below the upstream migration notes are resolved against our fixed Mathlib revision, not treated as new local leaves.