Megrez moves textbook topology formalization into an MK set-theory library: 262 files and 2,529 Qed proofs indexed

Textbook formalization no longer rests on a general coding agent plus proof-assistant tools alone; the agent first queries a knowledge graph rebuilt from Rocq sources, compiler references and curated metadata, then enters proving. The earlier general-agent route had shown results on standalone competition problems and research-level formalization, but low-resource MK set-theory libraries rarely appear in pretraining data, and textbook concepts lack direct counterparts among library declarations. On the MKTopos corpus the graph indexes 3,894 declarations and 60,982 reference edges, 96.8% of them resolved precisely from compiler .glob files, and covers 56 concept clusters, 982 Chinese aliases and 54 textbook sections.

Proof search is cut into short bursts of 1 to 5 tactics, and the agent reads the proof state or error returned by Rocq after each burst instead of generating one long script. A long script built without intermediate feedback rests on states that may already be broken, while repeated local failures usually signal a flaw in the mathematical route or representation rather than a single mistyped tactic. Each goal keeps a branch ledger recording the key tactics, last valid state and blocking subgoal of abandoned routes; when failed branches reach an exponential checkpoint, structured reflection writes a revised proof sketch and search resumes automatically.

A proof enters the library only after passing statement fidelity, axiom auditing and a full project build, and multi-theorem batches carry a recoverable scheduling state machine. A single-file compile cannot catch a candidate proof that silently routes through another unproven Admitted placeholder in the same file, nor guarantee compatibility with the whole project. The system includes 39 test modules and 319 automated contract and fault-injection tests, all passing in continuous integration; end-to-end scenario tests cover parallel claims on dependent theorems in one .v file, rewrite_candidate and reverify recovery from crashes injected before and after source writing, and later theorems' context fingerprints surviving an earlier theorem's completion without false stale invalidation.

The demonstrated setting is the point-set topology corpus MKTopos, written in Rocq 9.1 over MK set theory, with 12 modules, 262 .v files, 3,894 declarations and 102,122 lines of proof script; the retrieval latency benchmarks use synthetic 10,000-node and 100,000-node databases generated to match the corpus distribution, not a library after real growth.

Retrieval quality depends on curated concepts and Chinese aliases, compiler .glob edges record symbol occurrences rather than minimal logical dependencies, and soundness ultimately rests on the Rocq kernel and axiom auditing; the candidate scope snapshot filters by node-set membership rather than full Rocq module and notation visibility, full-text IDF statistics span all configured corpora, and cooperative read-only workers share one workspace without replacing OS-level sandboxing for untrusted processes.