In this note we compare two kinds of systems that verify the correctness of mathematical developments: roof checking and proof construction by tactics and we propose to merge them in a single system.

翻译：本注记比较了两种用于验证数学发展正确性的系统：证明检查与策略式证明构造，并提议将二者融合为单一系统。