AI 中文总结
该研究针对固定信息结构博弈，证明其相关均衡收益集未必为闭集，构造了多类博弈实例，解决了斯廷奇科姆的猜想，且相关结果已在Lean中形式化。
AI 中文摘要
奥曼（1974）证明，无原子公共随机化装置可使固定信息结构博弈的可行收益集与均衡收益集呈凸性，并提出这些集合是否为闭集的问题。我们证明，在该问题未解决的所有情形中，这些集合未必是闭集。所有例子均由同一信息结构生成：两个公平符号序列，其坐标相关性递增至上限ρ<1，且不存在任何一对可分别测量的平方可积规则能达到该上限。对于每个0<ρ<1，该信息结构可生成三类结果：一是带公共随机化装置的三人博弈，其均衡收益集恰好为开区间{(0,0,t):-ρ<t<ρ}；二是带公共随机化装置的两人博弈，其均衡收益集呈凸性、满维且非闭集；三是无公共装置时的非闭可行收益集与均衡收益集，后者沿均衡路径（均衡中唯一最优反应仅在零事件下存在）的收益趋近于一个甚至不可行的向量。当存在不同但相互绝对连续的主观先验时，即使有客观公共随机化装置，可行收益集、所有ε-均衡收益集及诱导法则元组集也可能不闭。我们的构造还解决了斯廷奇科姆（2011）的一个猜想。主要结果及支撑引理均在Lean证明助手中形式化；附录记录了每个命题的精确覆盖范围，包括仅给出纸面证明的条款。
英文摘要
Aumann (1974) showed that an atomless public randomization device makes the feasible- and equilibrium-payoff sets of a game with a fixed information structure convex, and asked whether they are closed. We show that, in every case the question leaves open, they need not be. One information structure drives all the examples: two sequences of fair signs whose coordinate correlations increase to a ceiling $ρ<1$ that no pair of separately measurable square-integrable rules attains. For every $0<ρ<1$ it yields a three-player game with a public randomization device whose equilibrium-payoff set is exactly the open interval $\{(0,0,t):-ρ<t<ρ\}$; a two-player game with a public randomization device whose equilibrium-payoff set is convex, full dimensional, and not closed; and, without any public device, nonclosed feasible- and equilibrium-payoff sets, the latter along equilibria with unique best replies modulo null events whose payoffs approach a vector that is not even feasible. With distinct but mutually absolutely continuous subjective priors, even the feasible-payoff set can fail to be closed in the presence of an objective public randomization device, together with every $\varepsilon$-equilibrium payoff set and the set of induced law tuples. Our construction also allows us to resolve a conjecture of Stinchcombe (2011). The main results and the lemmas supporting them are formalized in the Lean proof assistant; an appendix records the exact coverage of each statement, including the clauses for which only a paper proof is given.
Comments29 pages. The main results and supporting lemmas are formalized in Lean 4; the Lean package is included as ancillary files
