AutoGraphForge: 迈向自动化图论发现

摘要

AutoGraphForge是一个在建流水线，用于自动提出、反驳、形式化并证明图论猜想。Graffiti3生成器以反例引导方式在初始几百个图、仅随反例增长的快照表上逐轮提出猜想；由559条经典与民间关系构成的新颖性过滤器用线性规划判断是否已被已知结果蕴含，幸存者再在约348,000个图（含House of Graphs不变量导出、至多9个顶点的连通图穷举、若干极值族与随机模型）上测试。在HPC集群上运行数轮后，6,522个猜想通过数据集、新颖性过滤与主动搜索；其中有二部图与正则图的消没数与边覆盖数间的非平凡关系，已手工证明。后续将每个幸存猜想翻译为Lean 4语句骨架；候选证明经固定mathlib4与自定义不变量前导做内核验证，并整合DeepSeek-Prover-V2-671B与OProver-32B两个神经证明器。流水线已通过初步检查，正在运行。