一句话：证明轨道有限线性不等式组的实数可解性与优化可判定，并证明整数版本不可判定。
论文研究轨道有限线性规划：约束由轨道有限集合上的线性不等式系统给出，可视为普通线性规划在带原子置换对称性的无限集合上的推广。作者给出判定过程，用于检查该系统是否存在实数解，并计算线性目标函数在解集上的最小值或最大值。进一步证明，若只考虑整数解，相应的可解性与优化问题不可判定。由此得到主要结论：轨道有限线性规划在实数域可判定，而轨道有限整数线性规划不可判定。
An infinite set is orbit-finite if, up to permutations of the underlying structure of atoms, it has only finitely many elements. We study a generalisation of linear programming where constraints are expressed by an orbit-finite system of linear inequalities. As our principal contribution we provide a decision procedure for checking if such a system has a real solution, and for computing the minimal/maximal value of a linear objective function over the solution set. We also show undecidability of these problems in case when only integer solutions are considered. Therefore orbit-finite linear programming is decidable, while orbit-finite integer linear programming is not.