{"id":"palomar/PALOMAR-2026-09-08-000002","url":"https://github.com/Arthur742Ramos/verified-regret-matching-lean/tree/52e2c3dbbd8308b11271daf2e4c5a80aebae1df7","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-08-000002-v1.json","repo":"https://github.com/Arthur742Ramos/verified-regret-matching-lean","tags":["cs.GT","msc:91A10","msc:91A26","game-theory","regret-minimization","zero-sum-games","formalization"],"score":0,"title":"Verified regret matching and finite-time equilibrium computation","trust":"high","domain":"cs.GT","source":"palomar","authors":["Arthur Freitas Ramos"],"reviews":0,"subject":"cs.GT","summary":"For finite nonempty action sets and unit-interval full-information payoffs, regret matching and regret matching+ have cumulative external regret at most the square root of the product of the number of actions and the horizon, against every fixed pure or mixed comparator. In finite two-player zero-sum matrix games, simultaneous self-play gives an explicit finite-time approximate Nash guarantee for uniformly averaged strategies. A finite-vector implementation is proved to reproduce the abstract averages. Square-root-free accuracy budgets and finite rational payoff inequalities certify…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-09-08","reactions":{},"formalized":true,"formalizes":[{"title":"MIT 6.S890, Lecture 5: Learning in Games: Algorithms (Part I)","identifier":"https://www.mit.edu/~gfarina/2024/6S890f24_L05_algo1/L05.pdf","relationship":"formalizes"},{"title":"MIT 6.S890, Lecture 4: Learning in Games: Foundations","identifier":"https://www.mit.edu/~gfarina/2024/6S890f24_L04_regret/L04.pdf","relationship":"formalizes"}]}