一句话：在原子集合框架下给出轨道有限线性方程组可解性的判定过程，并证明其生成向量空间具有轨道有限基。
本文研究原子集合（sets with atoms）中的轨道有限线性方程组，核心问题是判定这类无限但具有对称结构的方程组是否可解。作者进一步发展了由轨道有限集生成的向量空间理论，证明每个这样的向量空间都存在轨道有限基，这一性质是构造判定过程的关键工具。所提算法在温和可有效计算假设下适用于任意域甚至交换环，将给定轨道有限系统归约为若干有限系统：一般情况下归约出的有限系统数量为指数级，但当输入系统的原子维数固定时，数量降为多项式级。该工作为轨道有限线性代数提供了可判定性结果与基础性定理。
We study orbit-finite systems of linear equations, in the setting of sets with atoms. Our principal contribution is a decision procedure for solvability of such systems. The procedure works for every field (and even commutative ring) under mild effectiveness assumptions, and reduces a given orbit-finite system to a number of finite ones: exponentially many in general, but polynomially many when the atom dimension of input systems is fixed. Towards obtaining the procedure we push further the theory of vector spaces generated by orbit-finite sets, and show that each such vector space admits an orbit-finite basis. This fundamental property is a key tool in our development, but should be also of wider interest.