Lean/Mathlib を使って場の量子論 (QFT) を形式化するという新しい論文が出ました。AI や定理証明といったホットな話題に時間を費やすのは避けようとしていたのですが、今回は非常に多くの…