We describe a recently developed algebraic framework for proving first-order statements about linear operators by computations with noncommutative polynomials. Furthermore, we present our new SageMath package operator_gb, which offers functionality for automatising such computations. We aim to provide a practical understanding of our approach and the software through examples, while also explaining the completeness of the method in the sense that it allows to find algebraic proofs for every true first-order operator statement. We illustrate the capability of the framework in combination with our software by a case study on statements about the Moore-Penrose inverse, including classical facts and recent results, presented in an online notebook.

翻译：我们描述了一个近期发展的代数框架，通过非交换多项式的计算来证明关于线性算子的一阶陈述。此外，我们介绍了新的SageMath软件包operator_gb，该软件包提供了自动化此类计算的功能。我们旨在通过实例提供对方法及软件的实用理解，同时解释方法的完备性——即该方法能够为每一真实的一阶算子陈述找到代数证明。通过关于Moore-Penrose逆的陈述案例研究（涵盖经典事实与最新结果，并以在线笔记本形式呈现），我们展示了该框架与软件的联合能力。