用Lean4形式化罗素的《数学原理》

这个项目旨在使用Lean定理证明器形式化伯特兰·罗素教授的《数学原理》第一卷。目标是确保形式化与书中相应的定理清晰一致，避免混淆。该项目遵循罗素的证明过程，尽量避免添加额外的语句。作者还创建了一个新的战术`Syll`，以处理更一般的三段论形式。尽管《数学原理》被认为是“巨大的失败”，但作者认为这个形式化过程是一个丰富的学习体验。