Megrez把教科书拓扑形式化搬进MK集合论库：262个文件、2529条Qed证明已入库
核心概要
面向建立在Morse–Kelley集合论之上的Rocq库，Megrez把通用编码智能体与可重建的知识图谱、短促交互式证明循环和三项验收流程组合起来，用于逐章形式化教科书。在点集拓扑语料MKTopos上，它覆盖12个模块、262个.v文件、3894条声明和2529条完成的Qed证明，共102122行证明脚本；检索基准显示，在10万节点规模下精确标识符查询的p95延迟从72.29毫秒降到1.23毫秒。
深度剖析
教科书形式化不再只靠通用编码智能体加证明助手工具，而是让智能体先查一张由Rocq源码、编译器引用和人工元数据重建的知识图谱，再进入证明。 此前的通用智能体路线在独立竞赛题和研究级形式化上已有表现，但低资源MK集合论库很少出现在预训练数据中，教科书概念与库中声明之间缺少直接对应。 在MKTopos语料上，图谱索引了3894条声明、60982条引用边，其中96.8%由编译器.glob文件精确解析，并覆盖56个概念簇、982条中文别名和54节教科书条目。
证明搜索被切成每次1到5条策略的短促交互，智能体每步都读取Rocq返回的证明状态或错误，而不是一次性生成长脚本。 长脚本在没有中间反馈时会建立在已经失效的状态上，而反复的局部失败往往说明数学路线或表示方式有问题，而非单条策略写错。 每个目标维护一份分支台账，记录被放弃路线的关键策略、最后有效状态和阻塞子目标；失败分支达到指数间隔的检查点时触发结构化反思，重新写出证明草图后自动继续搜索。
一条证明要进入库，必须同时通过陈述保真、公理审计和全项目构建三项检查，多定理批次还带有可恢复的调度状态机。 单文件编译无法发现候选证明绕道同文件中另一个未证明的Admitted占位符，也无法保证新代码与整个项目兼容。 系统包含39个测试模块、319项自动化契约与故障注入测试，全部在持续集成中通过；端到端场景测试覆盖同一.v文件内依赖定理的并行认领、写入前后崩溃触发的rewrite_candidate与reverify恢复，以及前序定理完成后后续定理上下文指纹不被误判失效。
启示与展望
演示范围是建立在MK集合论之上、用Rocq 9.1编写的点集拓扑语料MKTopos，共12个模块、262个.v文件、3894条声明和102122行证明脚本；检索延迟基准使用按语料分布生成的1万节点与10万节点合成数据库，而非真实增长后的库。
检索质量依赖人工整理的概念与中文别名，编译器.glob边记录的是符号出现而非最小逻辑依赖，可靠性最终仍由Rocq内核与公理审计承担；候选范围快照按节点集合成员资格过滤，而非完整的Rocq模块与记号可见性，全文IDF统计跨越所有已配置语料；协作式只读工作进程共享同一工作区，不替代针对不可信进程的操作系统级沙箱。