我的第一个 Isabelle 形式化证明
有些证明想被刻在更坚固的地方。
纸上的推导可以泛黄，黑板上的公式终将被擦去，但形式化证明留下的，是可以被反复验证的真理。
我在做的主题
我目前研究的方向和 submodular function 以及 greedy algorithm 相关。具体来说，我正在尝试形式化 Nemhauser–Wolsey theorem 的证明，这是一条关于单调子模函数的贪心近似比保证的经典结果。
我要在 Isabelle 里完成：
把数学对象抽象成形式化定义（函数、集合、单调性、子模性…）
搭建推理框架
写出与数学证明完全等价的 machine-checkable version。
就像在对话一样，我要让 Isabelle 听懂我想说的话（但它不会宽容我任何一个跳步或模糊表达XD
为什么我选择 Isabelle（而不是 Lean）
数学本身就是严谨的，但人类的证明往往带着直觉和省略。而 Isabelle 逼着我去把直觉全部拆解成可验证的语句，这个过程虽然痛苦，但很真实（其实是我老师做 Isabelle ）
它让我看到了：
哪些我以为显然的步骤其实需要补充
哪些论证的逻辑关系是我自己没意识到的
证明结构如何在形式化中变得「可复用」
对我而言，这不仅仅是完成一个 formal proof，更像是学习“如何更诚实地写数学”。
目前进展
✔ 已完成：
定义 filter limit 与 sequential limit
证明 filter limit 蕴含 sequential limit
建立贪心算法的基本形式化骨架
🚧 进行中：
证明两种极限定义的等价性
抽象出子模函数贪心近似的核心逻辑
❌ 未来计划：
完整复刻并扩展 Nemhauser–Wolsey 的形式化证明
尝试将优化理论与形式化工具结合