We introduce and elaborate a novel formalism for the manipulation and analysis of proofs as objects in a global manner. In this first approach the formalism is restricted to first-order problems characterized by condensed detachment. It is applied in an exemplary manner to a coherent and comprehensive formal reconstruction and analysis of historical proofs of a widely-studied problem due to {\L}ukasiewicz. The underlying approach opens the door towards new systematic ways of generating lemmas in the course of proof search to the effects of reducing the search effort and finding shorter proofs. Among the numerous reported experiments along this line, a proof of {\L}ukasiewicz's problem was automatically discovered that is much shorter than any proof found before by man or machine.

翻译：我们提出并详细阐述了一种新颖的形式化方法，用于以全局方式操作和分析作为对象的证明。在此初步方法中，该形式化仅限于以压缩分离为特征的一阶问题。它以示例性方式应用于对一个广泛研究的、由Łukasiewicz提出的问题的历史证明进行连贯而全面的形式化重构与分析。所提出的方法为在证明搜索过程中以系统方式生成引理开辟了新途径，从而减少搜索工作量并找到更短的证明。在众多相关实验中，自动发现了一个比之前任何人或机器找到的证明都短得多的Łukasiewicz问题证明。