数学能被机器"翻译"，法律为什么不行？

最近看到一篇关于法律自动化形式化的讨论，挺有意思。数学里，非形式化的证明可以被机器转成可验证的形式化定理——Lean、Coq这些工具已经证明了这条路走得通。那法律呢？为什么同样的思路在法律领域几乎碰壁？我的判断是：法律的本质不在逻辑链条，而在语义模糊和情境判断。数学定理要么是0要么是1，但法条的解释空间大得惊人。试图把法律塞进形式化的壳子里，更像是削足适履。这不是技术问题，是本体论的鸿沟。

原文：The auto-formalization of mathematics versus law · 来源：Hacker News