AutoGraphForge 构建“猜想—反例—形式化—证明”的自动图论发现闭环

AutoGraphForge 报告了一个自动图论研究 pipeline：生成猜想后以反例扩充图数据，使用经典关系 novelty filter、约 34.8 万个图的测试集和主动反例搜索进行筛选，再将候选确定性转换为 Lean 4 statement skeleton，并接入 DeepSeek-Prover-V2-671B 与 OProver-32B，在 Lean kernel 下独立验证。作者报告多轮运行得到 6,522 个经当前反驳流程存活的猜想。