[1/3] 终于完成了无类型 λ-演算中 Böhm 分离定理的形式化证明，改进了去年 ITP 2025 论文里给出一个较弱的结果。一个多月时间，1万多行新代码，不简单，因为前面证的所有那些引理（根据直觉）究竟有没有用，只有到了最后一天才能知道。那些在其他定理证明器里搞 λ-演算形式化的人，我只能呵呵了，几万行代码的技术差距足以让一个自由选择研究方向同时想尽快出论文的人放弃了。
发布于 辽宁
田春冰河