{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,17]],"date-time":"2026-04-17T11:03:15Z","timestamp":1776423795890,"version":"3.51.2"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2025,10,15]],"date-time":"2025-10-15T00:00:00Z","timestamp":1760486400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,15]],"date-time":"2025-10-15T00:00:00Z","timestamp":1760486400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,12]]},"DOI":"10.1007\/s10817-025-09741-w","type":"journal-article","created":{"date-parts":[[2025,10,15]],"date-time":"2025-10-15T11:36:30Z","timestamp":1760528190000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formalization of Convergence Rates of Four First-order Algorithms for Convex Optimization"],"prefix":"10.1007","volume":"69","author":[{"given":"Chenyi","family":"Li","sequence":"first","affiliation":[]},{"given":"Ziyu","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Wanyi","family":"He","sequence":"additional","affiliation":[]},{"given":"Yuxuan","family":"Wu","sequence":"additional","affiliation":[]},{"given":"Shengyang","family":"Xu","sequence":"additional","affiliation":[]},{"given":"Zaiwen","family":"Wen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,10,15]]},"reference":[{"issue":"2","key":"9741_CR1","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/s10817-018-9477-1","volume":"63","author":"X Allamigeon","year":"2019","unstructured":"Allamigeon, X., Katz, R.D.: A formalization of convex polyhedra based on the simplex method. J. Automat. Reason. 63(2), 323\u2013345 (2019). https:\/\/doi.org\/10.1007\/s10817-018-9477-1","journal-title":"J. Automat. Reason."},{"issue":"4","key":"9741_CR2","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/s10817-017-9404-x","volume":"59","author":"J Avigad","year":"2017","unstructured":"Avigad, J., H\u00f6lzl, J., Serafin, L.: A formally verified proof of the central limit theorem. J. Autom. Reason. 59(4), 389\u2013423 (2017)","journal-title":"J. Autom. Reason."},{"key":"9741_CR3","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611974997","volume-title":"First-Order Methods in Optimization","author":"A Beck","year":"2017","unstructured":"Beck, A.: First-Order Methods in Optimization. SIAM-Society for Industrial and Applied Mathematics, Philadelphia, PA, USA (2017)"},{"issue":"1","key":"9741_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1137\/080716542","volume":"2","author":"A Beck","year":"2009","unstructured":"Beck, A., Teboulle, M.: A fast iterative shrinkage-thresholding algorithm for linear inverse problems. SIAM J. Imag. Sci. 2(1), 183\u2013202 (2009)","journal-title":"SIAM J. Imag. Sci."},{"key":"9741_CR5","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-031-30820-8_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Bentkamp","year":"2023","unstructured":"Bentkamp, A., Mir, R.F., Avigad, J.: Verified reductions for optimization. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 74\u201392. Springer, Cham (2023)"},{"key":"9741_CR6","doi-asserted-by":"publisher","first-page":"1196","DOI":"10.1017\/S0960129514000437","volume":"26","author":"S Boldo","year":"2015","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Formalization of real analysis: a survey of proof assistants and libraries $$\\dagger $$. Math. Struct. Comput. Sci. 26, 1196\u20131233 (2015)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1\u20132","key":"9741_CR7","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/s10107-013-0701-9","volume":"146","author":"J Bolte","year":"2014","unstructured":"Bolte, J., Sabach, S., Teboulle, M.: Proximal alternating linearized minimization for nonconvex and nonsmooth problems. Math. Program. 146(1\u20132), 459\u2013494 (2014)","journal-title":"Math. Program."},{"issue":"2","key":"9741_CR8","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1137\/16M1080173","volume":"60","author":"L Bottou","year":"2018","unstructured":"Bottou, L., Curtis, F.E., Nocedal, J.: Optimization methods for large-scale machine learning. SIAM Rev. 60(2), 223\u2013311 (2018)","journal-title":"SIAM Rev."},{"key":"9741_CR9","doi-asserted-by":"crossref","unstructured":"Boyd, S.P., Vandenberghe, L.: Convex Optimization. Cambridge university press, Cambridge, CB2 8RU, UK (2004)","DOI":"10.1017\/CBO9780511804441"},{"key":"9741_CR10","unstructured":"Boyd, S., Xiao, L., Mutapcic, A.: Subgradient methods. lecture notes of EE392o, Stanford University, Autumn Quarter 2004(01) (2003)"},{"key":"9741_CR11","doi-asserted-by":"publisher","unstructured":"Community, T.: The lean mathematical library. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2020, pp. 367\u2013381. Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"},{"key":"9741_CR12","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Kong, S., Avigad, J., Van\u00a0Doorn, F., Raumer, J.: The lean theorem prover (system description). In: Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pp. 378\u2013388 (2015). Springer","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"9741_CR13","doi-asserted-by":"crossref","unstructured":"Gou\u00ebzel, S.: A formalization of the change of variables formula for integrals in mathlib. In: International Conference on Intelligent Computer Mathematics, pp. 3\u201318 (2022). Springer","DOI":"10.1007\/978-3-031-16681-5_1"},{"key":"9741_CR14","unstructured":"Grechuk, B.: Lower semicontinuous functions. Archive of Formal Proofs (2011). https:\/\/isa-afp.org\/entries\/Lower_Semicontinuous.html, Formal proof development"},{"key":"9741_CR15","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-642-39634-2_21","volume-title":"Interactive Theorem Proving","author":"J H\u00f6lzl","year":"2013","unstructured":"H\u00f6lzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in isabelle\/hol. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving, pp. 279\u2013294. Springer, Berlin, Heidelberg (2013)"},{"key":"9741_CR16","unstructured":"Kudryashov, Y.: Formalizing the divergence theorem and the cauchy integral formula in lean. In: 13th International Conference on Interactive Theorem Proving (ITP 2022) (2022). Schloss-Dagstuhl-Leibniz Zentrum f\u00fcr Informatik"},{"key":"9741_CR17","volume-title":"Optimization: Modeling","author":"H Liu","year":"2020","unstructured":"Liu, H., Hu, J., Li, Y., Wen, Z.: Optimization: Modeling. Algorithm and Theory. higher education press, Beijing, China (2020)"},{"key":"9741_CR18","doi-asserted-by":"crossref","unstructured":"Nesterov, Y.: Lectures on Convex Optimization, 2nd edn. Springer, Gewerbestrasse 11, 6330 Cham, Switzerland (2018)","DOI":"10.1007\/978-3-319-91578-4"},{"issue":"3","key":"9741_CR19","first-page":"543","volume":"269","author":"Y Nesterov","year":"1983","unstructured":"Nesterov, Y.: A method of solving a convex programming problem with convergence rate o (1\/k** 2). Dokl. Akad. Nauk SSSR 269(3), 543 (1983)","journal-title":"Dokl. Akad. Nauk SSSR"},{"key":"9741_CR20","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: A proof assistant for higher-order logic. Lecture Notes in Computer Science (2002)"},{"key":"9741_CR21","doi-asserted-by":"crossref","unstructured":"Nocedal, J., Wright, S.J.: Numerical Optimization, 2nd edn. Springer, New York, NY 10013, USA (1999)","DOI":"10.1007\/b98874"},{"issue":"3","key":"9741_CR22","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1561\/2400000003","volume":"1","author":"N Parikh","year":"2014","unstructured":"Parikh, N., Boyd, S., et al.: Proximal algorithms. Foundations and trends \u00ae in Optimization 1(3), 127\u2013239 (2014)","journal-title":"Foundations and trends \u00ae in Optimization"},{"issue":"2","key":"9741_CR23","doi-asserted-by":"publisher","first-page":"1126","DOI":"10.1137\/120891009","volume":"23","author":"M Razaviyayn","year":"2013","unstructured":"Razaviyayn, M., Hong, M., Luo, Z.-Q.: A unified convergence analysis of block successive minimization methods for nonsmooth optimization. SIAM J. Optim. 23(2), 1126\u20131153 (2013). https:\/\/doi.org\/10.1137\/120891009","journal-title":"SIAM J. Optim."},{"key":"9741_CR24","unstructured":"Sun, W., Yuan, Y.-X.: Optimization Theory and Methods: Nonlinear Programming vol. 1. Springer, New York, NY 10013, USA (2006)"},{"key":"9741_CR25","doi-asserted-by":"crossref","unstructured":"Tassarotti, J., Vajjha, K., Banerjee, A., Tristan, J.-B.: A formal proof of pac learnability for decision stumps. In: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 5\u201317 (2021)","DOI":"10.1145\/3437992.3439917"},{"key":"9741_CR26","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-031-42753-4_14","volume-title":"Intelligent Computer Mathematics","author":"M Tekriwal","year":"2023","unstructured":"Tekriwal, M., Appel, A.W., Kellison, A.E., Bindel, D., Jeannin, J.-B.: Verified correctness, accuracy, and convergence of a stationary iterative linear solver: jacobi method. In: Dubois, C., Kerber, M. (eds.) Intelligent Computer Mathematics, pp. 206\u2013221. Springer, Cham (2023)"},{"key":"9741_CR27","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-031-60698-4_3","volume-title":"NASA Formal Methods","author":"M Tekriwal","year":"2024","unstructured":"Tekriwal, M., Miller, J., Jeannin, J.-B.: Formalization of asymptotic convergence for stationary iterative methods. In: Benz, N., Gopinath, D., Shi, N. (eds.) NASA Formal Methods, pp. 37\u201356. Springer, Cham (2024)"},{"issue":"none","key":"9741_CR28","doi-asserted-by":"publisher","first-page":"1456","DOI":"10.1214\/13-EJS815","volume":"7","author":"RJ Tibshirani","year":"2013","unstructured":"Tibshirani, R.J.: The lasso problem and uniqueness. Electronic Journal of Statistics 7(none), 1456\u20131490 (2013). https:\/\/doi.org\/10.1214\/13-EJS815","journal-title":"Electronic Journal of Statistics"},{"key":"9741_CR29","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/s10915-018-0757-z","volume":"78","author":"Y Wang","year":"2019","unstructured":"Wang, Y., Yin, W., Zeng, J.: Global convergence of admm in nonconvex nonsmooth optimization. J. Sci. Comput. 78, 29\u201363 (2019)","journal-title":"J. Sci. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09741-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09741-w","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09741-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T08:50:26Z","timestamp":1766134226000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09741-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,15]]},"references-count":29,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["9741"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09741-w","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,15]]},"assertion":[{"value":"21 July 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 September 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 October 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no conflict of interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"28"}}