Tiancheng Xu

面向建立在Morse–Kelley集合论之上的Rocq库，Megrez把通用编码智能体与可重建的知识图谱、短促交互式证明循环和三项验收流程组合起来，用于逐章形式化教科书。在点集拓扑语料MKTopos上，它覆盖12个模块、262个.v文件、3894条声明和2529条完成的Qed证明，共102122行证明脚本；检索基准显示，在10万节点规模下精确标识符查询的p95延迟从72.29毫秒降到1.23毫秒。

面向建立在Morse–Kelley集合论之上的Rocq库，Megrez把通用编码智能体与可重建的知识图谱、短促交互式证明循环和三项验收流程组合起来，用于逐章形式化教科书。在点集拓扑语料MKTopos上，它覆盖12个模块、262个.v文件、3894条声明和2529条完成的Qed证明，共102122行证明脚本；检索基准显示，在10万节点规模下精确标识符查询的p95延迟从72.29毫秒降到1.23毫秒。