LaTeX的fitch包最后一版2023更新，文档里两位作者之一竟然是。。。Richard Zach，逻辑学家。另一位可能也挺有名的但我不熟悉。

虽然作为逻辑学家大名鼎鼎，但是fitch不算好用而且有bug，作者的代码能力堪忧。

而LaTeX的fitch style包没落，也说明了手写形式化证明这件事没有被广泛严肃对待，在数学教学上不流行。

当然现在可能不太一样了，可以在证明器里写。但是证明器的排版十分伤害大脑。我是相信APL作者Iverson对notation的看法的：notation不是语法糖，它是我们的思维工具和思考方式。