HEXAGONbeta

The Logical Anatomy of Optimization: Reverse Mathematics, Proof Mining, and the Price of Convergence

Primarily AI-generated textHuman understanding: some partsmath.LO — Logicmath.OC — Optimization and Controlcs.CC — Computational Complexitycs.LO — Logic in Computer Science

Contributed by Xiaoyu Li ↗

Version 1 / Nov 10, 2026 / CC BY 4.0

Abstract

Optimization theory proves three kinds of theorems: that optimal points exist, that algorithms converge to them, and that optimality can be certified by duality. We measure how much mathematics each kind needs, using reverse mathematics, Weihrauch complexity and proof mining, and assemble the answers, old and new, into one map stated in the language of optimization. Compactness makes existence cost weak Kőnig's lemma, but convexity (and, format by format, tameness) makes it cheap: we show that RCA0\mathsf{RCA}_0 proves that convex functions on [0,1][0,1] attain their minima (and on [0,1]n[0,1]^n, for each fixed nn, given a modulus of uniform continuity), and that RCA0\mathsf{RCA}_0 proves linear programming duality and the minimax theorem for real data of every size. Convergence costs more: it follows from results of Kohlenbach and Neumann that convergence of gradient descent for convex smooth functions on R\mathbb{R} is equivalent to ACA0\mathsf{ACA}_0. We explain this by a selection principle: what costs is the particular minimizer the algorithm selects, and uniqueness or an error bound removes the cost. Below convergence lies finitary information. Gradient descent in Rd\mathbb{R}^d has at most 2CdD/ε2C_dD/\varepsilon fluctuations of size ε\varepsilon, with CdC_d depending only on dd, which yields rates of metastability; no such bound is dimension-free, by the span-restriction argument behind performance estimation; and the limits of gradient descent on computable instances have d.c.e. coordinates, a proper subclass of the limit-computable reals. The map also covers Ekeland's variational principle (up to Π11-CA0\Pi^1_1\text{-}\mathsf{CA}_0), separation theorems, Kőnig duality (ATR0\mathsf{ATR}_0), proof-mined rates for fixed-point iterations, and the feasible world, where local search captures the NP\mathsf{NP} search problems provably total in T21T^1_2 and approximate stationary points of smooth functions are complete for CLS=PPAD∩PLS\mathsf{CLS}=\mathsf{PPAD}\cap\mathsf{PLS}. We close with five principles and open problems.

Provenance statement

This work was produced on 18 October 2026 with Claude Opus 5.5 (Anthropic), working as an agent in Claude Code. The submitting contributor posed the question of how reverse mathematics bears on optimization and delegated the remaining decisions. Claude chose the results, proved them, wrote the text and drew the figures. Separate Claude agents searched the literature in five lanes, ran novelty checks against the existing literature, checked every citation against its source, attacked the new results as adversaries, and reviewed the paper as referees; the paper was revised after each audit. The Specker-type gradient-descent construction behind Figure 2 was computed in 80-digit decimal arithmetic, and the staircase lower bound was checked numerically; these scripts are in anc/. The results the paper identifies as new are Theorem 3.2 (convex minimization in RCA_0) and Theorem 6.1 (LP duality and the minimax theorem in RCA_0 for every size); the other results are known or folklore, and Table 1 lists their sources. No part of this paper is formally verified.

Tools used

Anthropic
Claude OpusVersion 5.5
Anthropic
Claude Code
Python Software Foundation
Python 3 (numerical checks in anc/)

References

  1. Ron Aharoni, Menachem Magidor, and Richard A. Shore. On the strength of K ö nig's duality theorem for infinite bipartite graphs. Journal of Combinatorial Theory, Series B , 54 0 (2): 0 257--290, 1992. 10.1016/0095-8956(92)90057-5.DOI
  2. Ron Aharoni, Eli Berger, Agelos Georgakopoulos, Amitai Perlstein, and Philipp Spr ü ssel. The M ax- F low M in- C ut theorem for countable networks. Journal of Combinatorial Theory, Series B , 101 0 (1): 0 1--17, 2011. 10.1016/j.jctb.2010.08.002.DOI
  3. Klaus Ambos-Spies, Klaus Weihrauch, and Xizhong Zheng. Weakly computable real numbers. Journal of Complexity , 16 0 (4): 0 676--690, 2000. 10.1006/jcom.2000.0561.DOI
  4. Hedy Attouch, J é r ô me Bolte, and Benar Fux Svaiter. Convergence of descent methods for semi-algebraic and tame problems: proximal algorithms, forward--backward splitting, and regularized G auss-- S eidel methods. Mathematical Programming , 137 0 (1--2): 0 91--129, 2013.
  5. Jeremy Avigad and Jason Rute. Oscillation and the mean ergodic theorem for uniformly convex B anach spaces. Ergodic Theory and Dynamical Systems , 35 0 (4): 0 1009--1027, 2015. 10.1017/etds.2013.90.DOI
  6. Jeremy Avigad and Ksenija Simic. Fundamental notions of analysis in subsystems of second-order arithmetic. Annals of Pure and Applied Logic , 139 0 (1--3): 0 138--184, 2006. 10.1016/j.apal.2005.03.004.DOI
  7. Jean-Bernard Baillon and Ronald E. Bruck. The rate of asymptotic regularity is O(1/n)O(1/\sqrt{n}) . In Theory and Applications of Nonlinear Operators of Accretive and Monotone Type , volume 178 of Lecture Notes in Pure and Applied Mathematics , pages 51--81. Dekker, New York, 1996.
  8. Boaz Barak and David Steurer. Sum-of-squares proofs and the quest toward optimal algorithms. In Proceedings of the International Congress of Mathematicians (ICM 2014), Seoul , 2014.
  9. Heinz H. Bauschke, Eva Matou š kov á , and Simeon Reich. Projection and proximal point methods: convergence results and counterexamples. Nonlinear Analysis , 56: 0 715--738, 2004. 10.1016/j.na.2003.10.010. URL https://www.math.utoronto.ca/almut/MAT1000/P1P2-2004.pdf.DOI
  10. Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi, and Robert Robere. Stabbing planes. In 9th Innovations in Theoretical Computer Science Conference (ITCS 2018) , volume 94 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 10:1--10:20, 2018. 10.4230/LIPIcs.ITCS.2018.10.DOI
Show all 171 referencesShow fewer references
  1. Arnold Beckmann and Samuel R. Buss. Polynomial local search in the polynomial hierarchy and witnessing in fragments of bounded arithmetic. Journal of Mathematical Logic , 9 0 (1): 0 103--138, 2009. 10.1142/S0219061309000847.DOI
  2. Josef Berger and Hajime Ishihara. Brouwer's fan theorem and unique existence in constructive analysis. Mathematical Logic Quarterly , 51 0 (4): 0 360--364, 2005. 10.1002/malq.200410038.DOI
  3. Josef Berger and Gregor Svindland. A separating hyperplane theorem, the fundamental theorem of asset pricing, and Markov's principle. Annals of Pure and Applied Logic , 167 0 (11): 0 1161--1170, 2016 a . 10.1016/j.apal.2016.05.003.DOI
  4. Josef Berger and Gregor Svindland. Convexity and constructive infima. Archive for Mathematical Logic , 55 0 (7--8): 0 873--881, 2016 b . 10.1007/s00153-016-0502-y.DOI
  5. Josef Berger and Gregor Svindland. Brouwer's fan theorem and convexity. Journal of Symbolic Logic , 83 0 (4): 0 1363--1375, 2018. 10.1017/jsl.2018.49.DOI
  6. Josef Berger and Gregor Svindland. Convexity and unique minimum points. Archive for Mathematical Logic , 58 0 (1--2): 0 27--34, 2019. 10.1007/s00153-018-0619-2.DOI
  7. Josef Berger and Gregor Svindland. On Farkas' lemma and related propositions in BISH . Annals of Pure and Applied Logic , 173 0 (2): 0 103059, 2022. 10.1016/j.apal.2021.103059.DOI
  8. Josef Berger, Douglas Bridges, and Peter Schuster. The fan theorem and unique existence of maxima. Journal of Symbolic Logic , 71 0 (2): 0 713--720, 2006. 10.2178/jsl/1146620167.DOI
  9. Robert G. Bland. New finite pivoting rules for the simplex method. Mathematics of Operations Research , 2 0 (2): 0 103--107, 1977.
  10. Axel B ö hm and Aris Daniilidis. Ubiquitous algorithms in convex optimization generate self-contracted sequences. Journal of Convex Analysis , 29: 0 119--128, 2022.
  11. J é r ô me Bolte, Aris Daniilidis, and Adrian Lewis. The Ł ojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems. SIAM Journal on Optimization , 17 0 (4): 0 1205--1223, 2007.
  12. Vasco Brattka. Computability and analysis, a historical approach. In Arnold Beckmann, Laurent Bienvenu, and Nata š a Jonoska, editors, Pursuit of the Universal (CiE 2016) , Lecture Notes in Computer Science, pages 45--57. Springer, 2016. 10.1007/978-3-319-40189-8_5.DOI
  13. Vasco Brattka and Guido Gherardi. Effective choice and boundedness principles in computable analysis. The Bulletin of Symbolic Logic , 17 0 (1): 0 73--117, 2011 a . 10.2178/bsl/1294186663.DOI
  14. Vasco Brattka and Guido Gherardi. Weihrauch degrees, omniscience principles and weak computability. The Journal of Symbolic Logic , 76 0 (1): 0 143--176, 2011 b . 10.2178/jsl/1294170993.DOI
  15. Vasco Brattka, Peter Hertling, and Klaus Weihrauch. A tutorial on computable analysis. In S. Barry Cooper, Benedikt L ö we, and Andrea Sorbi, editors, New Computational Paradigms: Changing Conceptions of What is Computable , pages 425--491. Springer, 2008.
  16. Vasco Brattka, Matthew de Brecht, and Arno Pauly. Closed choice and a uniform low basis theorem. Annals of Pure and Applied Logic , 163 0 (8): 0 986--1008, 2012 a . 10.1016/j.apal.2011.12.020.DOI
  17. Vasco Brattka, Guido Gherardi, and Alberto Marcone. The B olzano-- W eierstrass theorem is the jump of weak K ő nig's lemma. Annals of Pure and Applied Logic , 163 0 (6): 0 623--655, 2012 b . 10.1016/j.apal.2011.10.006.DOI
  18. Vasco Brattka, St é phane Le Roux, Joseph S. Miller, and Arno Pauly. Connected choice and the Brouwer fixed point theorem. Journal of Mathematical Logic , 19 0 (1): 0 1950004, 2019. 10.1142/S0219061319500041.DOI
  19. Vasco Brattka, Guido Gherardi, and Arno Pauly. Weihrauch complexity in computable analysis. In Handbook of Computability and Complexity in Analysis , Theory and Applications of Computability, pages 367--417. Springer, 2021. 10.1007/978-3-030-59234-9_11.DOI
  20. Mario Bravo and Roberto Cominetti. Sharp convergence rates for averaged nonexpansive maps. Israel Journal of Mathematics , 227 0 (1): 0 163--188, 2018. 10.1007/s11856-018-1723-z.DOI
  21. Douglas K. Brown and Stephen G. Simpson. Which set existence axioms are needed to prove the separable Hahn-Banach theorem? Annals of Pure and Applied Logic , 31: 0 123--144, 1986. 10.1016/0168-0072(86)90066-7.DOI
  22. Samuel R. Buss and Jan Kraj í č ek. An application of B oolean complexity to separation problems in bounded arithmetic. Proceedings of the London Mathematical Society , s3-69 0 (1): 0 1--21, 1994. 10.1112/plms/s3-69.1.1.DOI
  23. Samuel R. Buss, Leszek Aleksander Kołodziejczyk, and Neil Thapen. Fragments of approximate counting. The Journal of Symbolic Logic , 79 0 (2): 0 496--525, 2014. 10.1017/jsl.2013.37.DOI
  24. Douglas Cenzer and Jeffrey B. Remmel. Proof-theoretic strength of the stable marriage theorem and other problems. In Stephen G. Simpson, editor, Reverse Mathematics 2001 , volume 21 of Lecture Notes in Logic , pages 67--103. Association for Symbolic Logic / Cambridge University Press, 2005. 10.1017/9781316755846.005.DOI
  25. Xi Chen, Xiaotie Deng, and Shang-Hua Teng. Settling the complexity of computing two-player N ash equilibria. Journal of the ACM , 56 0 (3): 0 1--57, 2009. 10.1145/1516512.1516516.DOI
  26. Hora ţ iu Cheval and Lauren ţ iu Leu ş tean. Linear rates of asymptotic regularity for H alpern-type iterations. Mathematics of Computation , 2024. 10.1090/mcom/3991.DOI
  27. Hora ţ iu Cheval, Ulrich Kohlenbach, and Lauren ţ iu Leu ş tean. On modified H alpern and T ikhonov- M ann iterations. Journal of Optimization Theory and Applications , 197 0 (1): 0 233--251, 2023. 10.1007/s10957-023-02192-6.DOI
  28. Va š ek Chv á tal. E dmonds polytopes and a hierarchy of combinatorial problems. Discrete Mathematics , 4 0 (4): 0 305--337, 1973. 10.1016/0012-365X(73)90167-2.DOI
  29. Peter G. Clote and Jeffry L. Hirst. Reverse mathematics of some topics from algorithmic graph theory. Fundamenta Mathematicae , 157 0 (1): 0 1--13, 1998. 10.4064/fm-157-1-1-13.DOI
  30. Roberto Cominetti, Jos é A. Soto, and Jos é Vaisman. On the rate of convergence of K rasnosel'ski ĭ - M ann iterations and their connection with sums of B ernoullis. Israel Journal of Mathematics , 199 0 (2): 0 757--772, 2014. 10.1007/s11856-013-0045-4.DOI
  31. Juan Pablo Contreras and Roberto Cominetti. Optimal error bounds for non-expansive fixed-point iterations in normed spaces. Mathematical Programming , 199 0 (1-2): 0 343--374, 2023. 10.1007/s10107-022-01830-7.DOI
  32. Stephen Cook and Phuong Nguyen. Logical Foundations of Proof Complexity . Cambridge University Press, 2010. ISBN 9780521517294. 10.1017/CBO9780511676277.DOI
  33. William J. Cook, Collette R. Coullard, and Gy ö rgy Tur á n. On the complexity of cutting-plane proofs. Discrete Applied Mathematics , 18 0 (1): 0 25--38, 1987. 10.1016/0166-218X(87)90039-4.DOI
  34. Daniel Dadush and Samarth Tiwari. On the complexity of branching proofs. In 35th Computational Complexity Conference (CCC 2020) , volume 169 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 34:1--34:35, 2020. 10.4230/LIPIcs.CCC.2020.34.DOI
  35. Aris Daniilidis, Olivier Ley, and St é phane Sabourau. Asymptotic behaviour of self-contracted planar curves and gradient orbits of convex functions. Journal de Math é matiques Pures et Appliqu é es , 94 0 (2): 0 183--199, 2010. 10.1016/j.matpur.2010.03.007.DOI
  36. Aris Daniilidis, Guy David, Estibalitz Durand-Cartagena, and Antoine Lemenant. Rectifiability of self-contracted curves in the E uclidean space and applications. The Journal of Geometric Analysis , 25 0 (2): 0 1211--1239, 2015. 10.1007/s12220-013-9464-z.DOI
  37. Constantinos Daskalakis and Christos Papadimitriou. Continuous local search. In Proceedings of the Twenty-Second Annual ACM-SIAM Symposium on Discrete Algorithms (SODA 2011) , pages 790--804, 2011. 10.1137/1.9781611973082.62.DOI
  38. Constantinos Daskalakis, Paul W. Goldberg, and Christos H. Papadimitriou. The complexity of computing a N ash equilibrium. SIAM Journal on Computing , 39 0 (1): 0 195--259, 2009. 10.1137/070699652.DOI
  39. Constantinos Daskalakis, Stratis Skoulakis, and Manolis Zampetakis. The complexity of constrained min-max optimization. In Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing (STOC 2021) , pages 1466--1478, 2021. 10.1145/3406325.3451125.DOI
  40. Bruno Dinis and Pedro Pinto. Quantitative results on the multi-parameters proximal point algorithm. Journal of Convex Analysis , 28 0 (3): 0 729--750, 2021. 10.68381/jca28041.DOI
  41. Yoel Drori and Marc Teboulle. Performance of first-order methods for smooth convex minimization: a novel approach. Mathematical Programming , 145 0 (1-2): 0 451--482, 2014. 10.1007/s10107-013-0653-0.DOI
  42. Damir D. Dzhafarov and Carl Mummert. Reverse Mathematics: Problems, Reductions, and Proofs . Theory and Applications of Computability. Springer, 2022.
  43. Ivar Ekeland. On the variational principle. Journal of Mathematical Analysis and Applications , 47 0 (2): 0 324--353, 1974.
  44. John Fearnley, Paul W. Goldberg, Alexandros Hollender, and Rahul Savani. The complexity of gradient descent: CLS = PPAD ∩\cap PLS . In Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing (STOC 2021) , pages 46--59, 2021. 10.1145/3406325.3451052.DOI
  45. John Fearnley, Paul W. Goldberg, Alexandros Hollender, and Rahul Savani. The complexity of computing KKT solutions of quadratic programs. In Proceedings of the 56th Annual ACM Symposium on Theory of Computing (STOC 2024) , pages 892--903, 2024. 10.1145/3618260.3649647.DOI
  46. Ant ó nio M. Fernandes and Fernando Ferreira. Groundwork for weak analysis. The Journal of Symbolic Logic , 67 0 (2): 0 557--578, 2002. 10.2178/jsl/1190150098.DOI
  47. Ariel Germ á n Fern á ndez and Michael Soltys. Feasible combinatorial matrix theory. In Krishnendu Chatterjee and Ji ř í Sgall, editors, Mathematical Foundations of Computer Science 2013 (MFCS) , Lecture Notes in Computer Science, pages 777--788. Springer, 2013. 10.1007/978-3-642-40313-2_68.DOI
  48. David Fern á ndez-Duque, Paul Shafer, and Keita Yokoyama. Ekeland's variational principle in weak and strong systems of arithmetic. Selecta Mathematica (N.S.) , 26 0 (5): 0 Art. 68, 2020. 10.1007/s00029-020-00597-z.DOI
  49. David Fern á ndez-Duque, Paul Shafer, Henry Towsner, and Keita Yokoyama. Metric fixed point theory and partial impredicativity. Philosophical Transactions of the Royal Society A , 381 0 (2248): 0 20220012, 2023. 10.1098/rsta.2022.0012.DOI
  50. Fernando Ferreira. A feasible theory for analysis. The Journal of Symbolic Logic , 59 0 (3): 0 1001--1011, 1994. 10.2307/2275924.DOI
  51. Noah Fleming, Mika G ö ö s, Russell Impagliazzo, Toniann Pitassi, Robert Robere, Li-Yang Tan, and Avi Wigderson. On the power and limitations of branch and cut. In 36th Computational Complexity Conference (CCC 2021) , volume 200 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 6:1--6:30, 2021. 10.4230/LIPIcs.CCC.2021.6.DOI
  52. Stephen Flood, Matthew Jura, Oscar Levin, and Tyler Markkanen. The computational strength of matchings in countable graphs. Annals of Pure and Applied Logic , 173 0 (8): 0 103133, 2022. 10.1016/j.apal.2022.103133.DOI
  53. Anton Freund and Nicholas Pischke. Effective rates for continuous-time quasi- F ej é r monotone dynamical systems, 2026.
  54. Anton Freund, Nicholas Pischke, and Patrick Uftring. Avoiding logical strength in real analysis, 2026.
  55. Harvey Friedman. Some systems of second order arithmetic and their use. In Proceedings of the International Congress of Mathematicians (Vancouver, 1974) , volume 1, pages 235--242. Canadian Mathematical Congress, 1975.
  56. Harvey Friedman. [ FOM ] constructive analysis. Foundations of Mathematics (FOM) mailing list, 13 May 2009, 2009. URL https://web.archive.org/web/2020/https://cs.nyu.edu/pipermail/fom/2009-May/013613.html.link
  57. Harvey M. Friedman, Stephen G. Simpson, and Rick L. Smith. Countable algebra and set existence axioms. Annals of Pure and Applied Logic , 25 0 (2): 0 141--181, 1983. 10.1016/0168-0072(83)90012-X.DOI
  58. Makoto Fujiwara, Kojiro Higuchi, and Takayuki Kihara. On the strength of marriage theorems and uniformity. Mathematical Logic Quarterly , 60 0 (3): 0 136--153, 2014. 10.1002/malq.201300021.DOI
  59. Philipp Gerhardy and Ulrich Kohlenbach. General logical metatheorems for functional analysis. Transactions of the American Mathematical Society , 360 0 (5): 0 2615--2660, 2008. 10.1090/S0002-9947-07-04429-7.DOI
  60. Guido Gherardi and Alberto Marcone. How incomputable is the separable Hahn-Banach theorem? Notre Dame Journal of Formal Logic , 50 0 (4): 0 393--425, 2009. 10.1215/00294527-2009-018.DOI
  61. Jun Le Goh. Some computability-theoretic reductions between principles around ATR0\mathsf{ATR}_0 , 2019.
  62. Mika G ö ö s, Pritish Kamath, Robert Robere, and Dmitry Sokolov. Adventures in monotone complexity and TFNP . In 10th Innovations in Theoretical Computer Science Conference (ITCS 2019) , volume 124 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 38:1--38:19, 2019. 10.4230/LIPIcs.ITCS.2019.38.DOI
  63. Mika G ö ö s, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, and Ran Tao. Further collapses in TFNP . In 37th Computational Complexity Conference (CCC 2022) , volume 234 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 33:1--33:15, 2022 a . 10.4230/LIPIcs.CCC.2022.33.DOI
  64. Mika G ö ö s, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, and Ran Tao. Separations in proof complexity and TFNP . In 2022 IEEE 63rd Annual Symposium on Foundations of Computer Science (FOCS) , pages 1150--1161, 2022 b . 10.1109/FOCS54457.2022.00111.DOI
  65. Daniel S. Gra ç a and Ning Zhong. The set of hyperbolic equilibria and of invertible zeros on the unit ball is computable. Theoretical Computer Science , 895: 0 48--54, 2021. 10.1016/j.tcs.2021.09.028.DOI
  66. Dima Grigoriev. Linear lower bound on degrees of P ositivstellensatz calculus proofs for the parity. Theoretical Computer Science , 259 0 (1--2): 0 613--622, 2001. 10.1016/S0304-3975(00)00157-2.DOI
  67. Dima Grigoriev and Nicolai Vorobjov. Complexity of N ull- and P ositivstellensatz proofs. Annals of Pure and Applied Logic , 113 0 (1--3): 0 153--160, 2001. 10.1016/S0168-0072(01)00055-0.DOI
  68. Chirag Gupta, Sivaraman Balakrishnan, and Aaditya Ramdas. Path length bounds for gradient descent and flow. Journal of Machine Learning Research , 22 0 (68): 0 1--63, 2021. URL https://jmlr.org/papers/v22/19-979.html.link
  69. Christopher S. Hardin and Daniel J. Velleman. The mean value theorem in second order arithmetic. Journal of Symbolic Logic , 66 0 (3): 0 1353--1358, 2001. 10.2307/2695111.DOI
  70. Denis R. Hirschfeldt. Slicing the Truth: On the Computable and Reverse Mathematics of Combinatorial Principles , volume 28 of Lecture Notes Series, Institute for Mathematical Sciences, National University of Singapore . World Scientific, 2014.
  71. Jeffry L. Hirst. Combinatorics in Subsystems of Second Order Arithmetic . PhD thesis, The Pennsylvania State University, 1987.
  72. Jeffry L. Hirst. Marriage theorems and reverse mathematics. In Logic and Computation (Pittsburgh, PA, 1987) , volume 106 of Contemporary Mathematics , pages 181--196. American Mathematical Society, Providence, RI, 1990. 10.1090/conm/106/1057822.DOI
  73. Jeffry L. Hirst and Carl Mummert. Reverse mathematics of matroids. In Adam Day, Michael Fellows, Noam Greenberg, Bakhadyr Khoussainov, Alexander Melnikov, and Frances Rosamond, editors, Computability and Complexity: Essays Dedicated to Rodney G. Downey on the Occasion of His 60th Birthday , volume 10010 of Lecture Notes in Computer Science , pages 143--159. Springer, 2017. 10.1007/978-3-319-50062-1_12.DOI
  74. Alan J. Hoffman. On approximate solutions of systems of linear inequalities. Journal of Research of the National Bureau of Standards , 49 0 (4): 0 263--265, 1952.
  75. A. James Humphreys and Stephen G. Simpson. Separation and weak K ö nig's lemma. Journal of Symbolic Logic , 64 0 (1): 0 268--278, 1999. 10.2307/2586763.DOI
  76. Hein S. Hundal. An alternating projection that does not converge in norm. Nonlinear Analysis: Theory, Methods & Applications , 57 0 (1): 0 35--61, 2004. 10.1016/j.na.2003.11.004.DOI
  77. Hajime Ishihara. An omniscience principle, the K ö nig lemma and the Hahn-Banach theorem. Zeitschrift f ü r Mathematische Logik und Grundlagen der Mathematik (Mathematical Logic Quarterly) , 36 0 (3): 0 237--240, 1990. 10.1002/malq.19900360307.DOI
  78. David S. Johnson, Christos H. Papadimitriou, and Mihalis Yannakakis. How easy is local search? Journal of Computer and System Sciences , 37 0 (1): 0 79--100, 1988. 10.1016/0022-0000(88)90046-3.DOI
  79. Attila Jo ó . Proof of N ash- W illiams' intersection conjecture for countable matroids. Advances in Mathematics , 380: 0 107608, 2021. 10.1016/j.aim.2021.107608.DOI
  80. William Julian and Fred Richman. A uniformly continuous function on [0,1] that is everywhere different from its infimum. Pacific Journal of Mathematics , 111 0 (2): 0 333--340, 1984. 10.2140/pjm.1984.111.333.DOI
  81. Takayuki Kihara. Incomputability of simply connected planar continua. Computability , 1 0 (2): 0 131--152, 2012. 10.3233/COM-12012.DOI
  82. Takayuki Kihara and Arno Pauly. Finite choice, convex choice and sorting. In T. V. Gopal and Junzo Watada, editors, Theory and Applications of Models of Computation (TAMC 2019) , volume 11436 of Lecture Notes in Computer Science , pages 378--393. Springer, 2019. 10.1007/978-3-030-14812-6_23.DOI
  83. Ulrich Kohlenbach. Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vall é e Poussin's proof for Chebycheff approximation. Annals of Pure and Applied Logic , 64 0 (1): 0 27--94, 1993 a . 10.1016/0168-0072(93)90213-W.DOI
  84. Ulrich Kohlenbach. New effective moduli of uniqueness and uniform a priori estimates for constants of strong unicity by logical analysis of known proofs in best approximation theory. Numerical Functional Analysis and Optimization , 14 0 (5-6): 0 581--606, 1993 b . 10.1080/01630569308816541.DOI
  85. Ulrich Kohlenbach. A quantitative version of a theorem due to B orwein- R eich- S hafrir. Numerical Functional Analysis and Optimization , 22 0 (5-6): 0 641--656, 2001. 10.1081/NFA-100105311.DOI
  86. Ulrich Kohlenbach. Uniform asymptotic regularity for M ann iterates. Journal of Mathematical Analysis and Applications , 279 0 (2): 0 531--544, 2003. 10.1016/S0022-247X(03)00028-3.DOI
  87. Ulrich Kohlenbach. Some logical metatheorems with applications in functional analysis. Transactions of the American Mathematical Society , 357 0 (1): 0 89--128, 2005. 10.1090/S0002-9947-04-03515-9.DOI
  88. Ulrich Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics . Springer Monographs in Mathematics. Springer, Berlin, Heidelberg, 2008. ISBN 978-3-540-77532-4. 10.1007/978-3-540-77533-1.DOI
  89. Ulrich Kohlenbach. On quantitative versions of theorems due to F . E . B rowder and R . W ittmann. Advances in Mathematics , 226 0 (3): 0 2764--2795, 2011. 10.1016/j.aim.2010.10.002.DOI
  90. Ulrich Kohlenbach. Proof-theoretic methods in nonlinear analysis. In Proceedings of the International Congress of Mathematicians (ICM 2018), Rio de Janeiro, Vol. 2 , pages 61--82. World Scientific, 2019 a . 10.1142/9789813272880_0045.DOI
  91. Ulrich Kohlenbach. On the reverse mathematics and Weihrauch complexity of moduli of regularity and uniqueness. Computability , 8 0 (3--4): 0 377--387, 2019 b . 10.3233/COM-180097.DOI
  92. Ulrich Kohlenbach. Quantitative analysis of a H alpern-type proximal point algorithm for accretive operators in B anach spaces. Journal of Nonlinear and Convex Analysis , 21: 0 2125--2138, 2020.
  93. Ulrich Kohlenbach. Quantitative results on the proximal point algorithm in uniformly convex B anach spaces. Journal of Convex Analysis , 28 0 (1): 0 11--18, 2021. 10.68381/jca28002.DOI
  94. Ulrich Kohlenbach. On the proximal point algorithm and its H alpern-type variant for generalized monotone operators in H ilbert space. Optimization Letters , 16 0 (2): 0 611--621, 2022. 10.1007/s11590-021-01738-9.DOI
  95. Ulrich Kohlenbach. Kreisel's ``shift of emphasis'' and contemporary proof mining. Studies in Logic , 16 0 (3): 0 1--35, 2023.
  96. Ulrich Kohlenbach. On the computational content of moduli of regularity and their logical strength. In Proceedings LTT 2026 , volume 441 of Electronic Proceedings in Theoretical Computer Science , pages 185--196, 2026. 10.4204/EPTCS.441.11.DOI
  97. Ulrich Kohlenbach and Lauren ţ iu Leu ş tean. Effective metastability of H alpern iterates in CAT (0) spaces. Advances in Mathematics , 231 0 (5): 0 2526--2556, 2012. 10.1016/j.aim.2012.06.028.DOI
  98. Ulrich Kohlenbach and Paulo Oliva. Proof mining in L1L_1 -approximation. Annals of Pure and Applied Logic , 121 0 (1): 0 1--38, 2003. 10.1016/S0168-0072(02)00081-7.DOI
  99. Ulrich Kohlenbach and Pedro Pinto. Quantitative translations for viscosity approximation methods in hyperbolic spaces. Journal of Mathematical Analysis and Applications , 507 0 (2): 0 125823, 2022. 10.1016/j.jmaa.2021.125823.DOI
  100. Ulrich Kohlenbach and Pedro Pinto. Fej é r monotone sequences revisited. Journal of Convex Analysis , 33 0 (1-2): 0 75--90, 2026. 10.68381/jca33005.DOI
  101. Ulrich Kohlenbach and Nicholas Pischke. Proof theory and non-smooth analysis. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences , 381 0 (2248): 0 20220015, 2023. 10.1098/rsta.2022.0015.DOI
  102. Ulrich Kohlenbach and Pavol Safarik. Fluctuations, effective learnability and metastability in analysis. Annals of Pure and Applied Logic , 165 0 (1): 0 266--304, 2014. 10.1016/j.apal.2013.07.014. URL https://www2.mathematik.tu-darmstadt.de/~kohlenbach/mind_ps_revised.pdf.DOI
  103. Ulrich Kohlenbach, Lauren ţ iu Leu ş tean, and Adriana Nicolae. Quantitative results on F ej é r monotone sequences. Communications in Contemporary Mathematics , 20 0 (2): 0 1750015, 2018. 10.1142/S0219199717500158.DOI
  104. Ulrich Kohlenbach, Genaro L ó pez-Acedo, and Adriana Nicolae. Moduli of regularity and rates of convergence for Fej é r monotone sequences. Israel Journal of Mathematics , 232 0 (1): 0 261--297, 2019. 10.1007/s11856-019-1870-x.DOI
  105. Leszek Aleksander Kołodziejczyk and Neil Thapen. The strength of the dominance rule, 2024.
  106. Leszek Aleksander Kołodziejczyk, Phuong Nguyen, and Neil Thapen. The provably total NP search problems of weak second order bounded arithmetic. Annals of Pure and Applied Logic , 162 0 (6): 0 419--446, 2011. 10.1016/j.apal.2010.12.002.DOI
  107. Andreas Kontogiannis, Ioannis Panageas, and Vasilis Pollatos. The computational complexity of avoiding strict saddle points in constrained optimization, 2026.
  108. Krzysztof Kurdyka. On gradients of functions definable in o-minimal structures. Annales de l'Institut Fourier , 48 0 (3): 0 769--783, 1998.
  109. Jean B. Lasserre. Global optimization with polynomials and the problem of moments. SIAM Journal on Optimization , 11 0 (3): 0 796--817, 2001. 10.1137/S1052623400366802.DOI
  110. Dai Tri Man Le and Stephen A. Cook. Formalizing randomized matching algorithms. Logical Methods in Computer Science , 8 0 (3), 2012. 10.2168/LMCS-8(3:5)2012.DOI
  111. St é phane Le Roux and Arno Pauly. Finite choice, convex choice and finding roots. Logical Methods in Computer Science , 11 0 (4): 0 Paper 6, 2015. 10.2168/LMCS-11(4:6)2015.DOI
  112. St é phane Le Roux and Martin Ziegler. Singular coverings and non-uniform notions of closed set computability. Mathematical Logic Quarterly , 54 0 (5): 0 545--560, 2008. 10.1002/malq.200610058.DOI
  113. Yunseok Lee, Holger Boche, and Gitta Kutyniok. Computability of optimizers, 2023.
  114. Carlton E. Lemke and Joseph T. Howson, Jr. Equilibrium points of bimatrix games. Journal of the Society for Industrial and Applied Mathematics , 12 0 (2): 0 413--423, 1964.
  115. Lauren ţ iu Leu ş tean. Rates of asymptotic regularity for H alpern iterations of nonexpansive mappings. Journal of Universal Computer Science , 13 0 (11): 0 1680--1691, 2007. 10.3217/jucs-013-11-1680.DOI
  116. Lauren ţ iu Leu ş tean and Pedro Pinto. Quantitative results on a H alpern-type proximal point algorithm. Computational Optimization and Applications , 79 0 (1): 0 101--125, 2021. 10.1007/s10589-021-00263-w.DOI
  117. Lauren ţ iu Leu ş tean, Adriana Nicolae, and Andrei Sipo ş . An abstract proximal point algorithm. Journal of Global Optimization , 72 0 (3): 0 553--577, 2018. 10.1007/s10898-018-0655-9.DOI
  118. Felix Lieder. On the convergence rate of the H alpern-iteration. Optimization Letters , 15 0 (2): 0 405--418, 2021. 10.1007/s11590-020-01617-9.DOI
  119. Henri Lombardi, Daniel Perrucci, and Marie-Fran ç oise Roy. An elementary recursive bound for effective P ositivstellensatz and H ilbert's 17th problem. Memoirs of the American Mathematical Society , 263 0 (1277), 2020. 10.1090/memo/1277.DOI
  120. Arkadi S. Nemirovsky and David B. Yudin. Problem Complexity and Method Efficiency in Optimization . Wiley-Interscience Series in Discrete Mathematics. Wiley, Chichester, New York, 1983. ISBN 0471103454.
  121. Morenikeji Neri and Nicholas Pischke. Proof mining and probability theory. Forum of Mathematics, Sigma , 13: 0 e187, 2025. 10.1017/fms.2025.10138.DOI
  122. Morenikeji Neri and Thomas Powell. On quantitative convergence for stochastic processes: Crossings, fluctuations and martingales. Transactions of the American Mathematical Society, Series B , 12: 0 974--1019, 2025. 10.1090/btran/229.DOI
  123. Morenikeji Neri and Thomas Powell. A quantitative R obbins- S iegmund theorem. The Annals of Applied Probability , 36 0 (1): 0 636--651, 2026. 10.1214/25-AAP2242.DOI
  124. Morenikeji Neri, Nicholas Pischke, and Thomas Powell. An abstract effective convergence theorem for stochastic processes, with applications to stochastic approximation, 2025.
  125. Morenikeji Neri, Nicholas Pischke, and Thomas Powell. Generalized fluctuation bounds for stochastic algorithms in the presence of compactness, 2026.
  126. Yurii Nesterov. Introductory Lectures on Convex Optimization: A Basic Course . Kluwer Academic Publishers, 2004.
  127. Eike Neumann. Computational problems in metric fixed point theory and their W eihrauch degrees. Logical Methods in Computer Science , 11 0 (4): 0 Paper 20, 2015. 10.2168/LMCS-11(4:20)2015.DOI
  128. Phuong The Nguyen. Bounded Reverse Mathematics . PhD thesis, University of Toronto, Graduate Department of Computer Science, 2008. URL https://eccc.weizmann.ac.il/static/books/Bounded_Reverse_Mathematics.link
  129. Ryan O'Donnell. SOS is not obviously automatizable, even approximately. In 8th Innovations in Theoretical Computer Science Conference (ITCS 2017) , volume 67 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 59:1--59:10, 2017. 10.4230/LIPIcs.ITCS.2017.59.DOI
  130. Christos H. Papadimitriou. On the complexity of the parity argument and other inefficient proofs of existence. Journal of Computer and System Sciences , 48 0 (3): 0 498--532, 1994. 10.1016/S0022-0000(05)80063-7.DOI
  131. Pablo A. Parrilo. Semidefinite programming relaxations for semialgebraic problems. Mathematical Programming , 96 0 (2): 0 293--320, 2003. 10.1007/s10107-003-0387-5.DOI
  132. Arno Pauly. How incomputable is finding Nash equilibria? Journal of Universal Computer Science , 16 0 (18): 0 2686--2710, 2010. 10.3217/jucs-016-18-2686.DOI
  133. NingNing Peng, Weiguang Peng, and Takeshi Yamazaki. Mixed N ash equilibria for continuous games and reverse mathematics. Quaestiones Mathematicae , 46 0 (4): 0 621--632, 2023. 10.2989/16073606.2022.2035448.DOI
  134. Weiguang Peng and Takeshi Yamazaki. Two kinds of fixed point theorems and reverse mathematics. Mathematical Logic Quarterly , 63 0 (5): 0 454--461, 2017. 10.1002/malq.201600096.DOI
  135. Nicholas Pischke. Logical metatheorems for accretive and (generalized) monotone set-valued operators. Journal of Mathematical Logic , 24 0 (2): 0 2350008, 2024. 10.1142/S0219061323500083.DOI
  136. Nicholas Pischke. Generalized F ej é r monotone sequences and their finitary content. Optimization , 74 0 (14): 0 3771--3838, 2025. 10.1080/02331934.2024.2390114.DOI
  137. Nicholas Pischke and Ulrich Kohlenbach. Quantitative analysis of a subgradient-type method for equilibrium problems. Numerical Algorithms , 90 0 (1): 0 197--219, 2022. 10.1007/s11075-021-01184-9.DOI
  138. Nicholas Pischke and Thomas Powell. Asymptotic regularity of a generalised stochastic H alpern scheme. Journal of Optimization Theory and Applications , 210 0 (1): 0 3, 2026. 10.1007/s10957-026-03032-z.DOI
  139. Pavel Pudl á k. Lower bounds for resolution and cutting plane proofs and monotone computations. The Journal of Symbolic Logic , 62 0 (3): 0 981--998, 1997. 10.2307/2275583.DOI
  140. Prasad Raghavendra and Benjamin Weitz. On the bit complexity of sum-of-squares proofs. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017) , volume 80 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 80:1--80:13, 2017. 10.4230/LIPIcs.ICALP.2017.80.DOI
  141. R. Tyrrell Rockafellar. Convex Analysis . Princeton University Press, 1970.
  142. Shoham Sabach and Shimrit Shtern. A first order method for solving convex bilevel optimization problems. SIAM Journal on Optimization , 27 0 (2): 0 640--660, 2017. 10.1137/16M105592X.DOI
  143. Grant Schoenebeck. Linear level L asserre lower bounds for certain kk- CSP s. In 2008 49th Annual IEEE Symposium on Foundations of Computer Science (FOCS) , pages 593--602, 2008. 10.1109/FOCS.2008.74.DOI
  144. Paul Shafer. Menger's theorem in Π11-CA0\Pi^1_1\text{-}\mathsf{CA}_0 . Archive for Mathematical Logic , 51 0 (3--4): 0 407--423, 2012. 10.1007/s00153-012-0269-8.DOI
  145. Naoki Shioji and Kazuyuki Tanaka. Fixed point theory in weak second-order arithmetic. Annals of Pure and Applied Logic , 47 0 (2): 0 167--188, 1990. 10.1016/0168-0072(90)90068-D.DOI
  146. Stephen G. Simpson. Which set existence axioms are needed to prove the Cauchy/Peano theorem for ordinary differential equations? Journal of Symbolic Logic , 49 0 (3): 0 783--802, 1984. 10.2307/2274131.DOI
  147. Stephen G. Simpson. On the strength of K ö nig's duality theorem for countable bipartite graphs. Journal of Symbolic Logic , 59 0 (1): 0 113--123, 1994. 10.2307/2275254.DOI
  148. Stephen G. Simpson. Subsystems of Second Order Arithmetic . Perspectives in Logic. Cambridge University Press / Association for Symbolic Logic, 2 edition, 2009. ISBN 978-0-521-88439-6. 10.1017/CBO9780511581007.DOI
  149. Andrei Sipo ş . Quantitative inconsistent feasibility for averaged mappings. Optimization Letters , 16 0 (6): 0 1915--1925, 2022. 10.1007/s11590-021-01812-2.DOI
  150. Michael Soltys and Stephen Cook. The proof complexity of linear algebra. Annals of Pure and Applied Logic , 130 0 (1--3): 0 277--323, 2004. 10.1016/j.apal.2003.10.018.DOI
  151. Ernst Specker. Nicht konstruktiv beweisbare S ä tze der A nalysis. The Journal of Symbolic Logic , 14 0 (3): 0 145--158, 1949. 10.2307/2267043.DOI
  152. Ernst Specker. Der S atz vom M aximum in der rekursiven A nalysis. In Arend Heyting, editor, Constructivity in Mathematics (Proc. Colloq. Amsterdam 1957) , Studies in Logic and the Foundations of Mathematics, pages 254--265. North-Holland, Amsterdam, 1959.
  153. Eugene Stepanov and Yana Teplitskaya. Self-contracted curves have finite length. Journal of the London Mathematical Society , 96 0 (2): 0 455--481, 2017. 10.1112/jlms.12068.DOI
  154. Terence Tao. Norm convergence of multiple ergodic averages for commuting transformations. Ergodic Theory and Dynamical Systems , 28 0 (2): 0 657--688, 2008. 10.1017/S0143385708000011.DOI
  155. Alfred Tarski. A Decision Method for Elementary Algebra and Geometry . University of California Press, 2 edition, 1951.
  156. Adrien B. Taylor, Julien M. Hendrickx, and Fran ç ois Glineur. Smooth strongly convex interpolation and exact worst-case performance of first-order methods. Mathematical Programming , 161 0 (1-2): 0 307--345, 2017. 10.1007/s10107-016-1009-3.DOI
  157. Henry Towsner. Partial impredicativity in reverse mathematics. Journal of Symbolic Logic , 78 0 (2): 0 459--488, 2013. 10.2178/jsl.7802070.DOI
  158. Iddo Tzameret and Stephen A. Cook. Uniform, integral, and feasible proofs for the determinant identities. Journal of the ACM , 68 0 (2): 0 1--80, 2021. 10.1145/3431922.DOI
  159. Klaus Weihrauch. Computable Analysis: An Introduction . Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin, 2000. 10.1007/978-3-642-56999-9.DOI
  160. Rainer Wittmann. Approximation of fixed points of nonexpansive mappings. Archiv der Mathematik , 58 0 (5): 0 486--491, 1992.
  161. Xizhong Zheng, Robert Rettinger, and George Barmpalias. h-monotonically computable real numbers. Mathematical Logic Quarterly , 51 0 (2): 0 157--170, 2005. 10.1002/malq.200410016.DOI

Version history

  1. v1 · 46 pagesSubmitted by Xiaoyu LiInitial depositCurrentNov 08, 2026