# Megrez: A Knowledge-Guided Agent for Formal Mathematics over MK Set Theory

**Authors:** Tiancheng Xu, Wensheng Yu  
**Published:** 10 Nov 2026  
**Links:** [arXiv](https://arxiv.org/abs/2611.13613) · [PDF](https://arxiv.org/pdf/2611.13613) · [This page](https://omen-bit.github.io/ai-paper-daily/paper/2611.13613.html)

## Abstract

General-purpose coding agents equipped with proof-assistant tools have shown strong performance on standalone competition problems, yet cumulative textbook formalization inside a low-resource mathematical library still faces three obstacles: aligning textbook concepts with library declarations, keeping long-horizon search synchronized with live proof states, and integrating locally verified proofs reliably into a growing codebase. We present Megrez, a knowledge-guided formalization agent for Rocq libraries built on Morse--Kelley (MK) set theory. Megrez coordinates a general coding agent through three mechanisms: (1) a source-rebuildable knowledge graph merging formal declarations, compiler references, and curated metadata to support retrieval via Chinese aliases, concept clusters, proof dependencies, and multi-lane full-text ranking; (2) a feedback-driven 1--5 tactic short-burst proving loop paired with a goal-local branch ledger and exponential-interval structured reflection; and (3) a three-check acceptance pipeline (statement fidelity, axiom auditing, and full builds) coupled with a multi-corpus Provider stack and a candidate-bound recoverable batch state machine. Deployment and evaluation on a point-set topology corpus demonstrate effective cross-chapter formalization and scalable premise retrieval.

---

Notes written by AI from the paper, numbers copied from the abstract. Check the paper before you rely on them. From AI Papers Daily.