博文

P vs NP 的证明的形式化验证已经公开发布

已有 1090 次阅读 2026-9-15 21:00 |系统分类:科研笔记

我们关于 P vs NP 的证明已经通过了形式化验证。

该形式化验证代码已经发布在Github上。

经典的bool版的P vs NP 存在信息论障碍以及半符号悖论。

符号版的P ≠ NP 命题成立。

项目	状态 / 数值
论文成果	“P≠NP”方向系列研究论文（测度篇、模型篇、哲学篇、障碍篇、回应篇等）
机器验证	8,712 个构建任务全部通过、0 错误（Lean 4.32.2）
声明公理 / 证明缺口	0 条 / 0 处
工程规模	57 个 Lean 文件、99,818 行
核心结论（经机器验证）	分离主定理及障碍精化版；符号层分离 P_sym0 ≠ NP_sym0；本质维度下界 κ ≥ n；验证器最坏步数界 O((\|x\|+1)²)
证明最终依赖	数学基础三公理（propext / Classical.choice / Quot.sound）；编译式证明依赖项 16,753 条（逐项披露，可复核）
独立验证	已独立验证（2026 年 9 月 14 日、15 日），技术声明全部证实
代码仓库	GitHub：zhengbojin/mp（公开）