Isabelle

Isabelle 是一个用于通过计算机编写和检查数学证明的辅助工具。
它允许用形式语言表达数学公式，并提供工具在逻辑演算中证明这些公式。