MerLean-Prover · Chapter 01

Keep the theorem fixed while the proof changes

The difficulty is not only finding a proof term. It is keeping track of the mathematical claim through many local decisions, failed attempts, and revised helper lemmas.

A proof is always a proof of a statement

MerLean-Prover starts from a Lean declaration whose proof is unfinished. Its name, parameters, assumptions, and conclusion form an anchor. The agent can introduce helper lemmas, but it must eventually fill the original proof obligation.

A compiler checks the declaration it receives. If an agent has quietly added an assumption or weakened a conclusion, a successful build can establish a different theorem. An independent statement check and an audit of the final proof’s dependencies address different parts of this problem.

Model

Adding the conclusion as an assumption changes the task

The left judgment is immediate: use the extra assumption $h$ . It illustrates why well-typed code alone cannot certify that an edited declaration still expresses the original task. This is an explanatory example, not the specific edit made in the Burnside run.

\Gamma,\ h:T\ \vdash\ h:T\qquad\text{does not establish}\qquad\Gamma\vdash p:T.

A concrete target: Burnside’s prime-degree theorem

Let $\Omega$ be a finite set with prime cardinality $p$ , and let $G\leq\operatorname{Sym}(\Omega)$ act transitively. Burnside’s theorem gives a sharp alternative: either the action is 2-transitive, or a normal subgroup already moves points in a regular way. This is the target of the paper’s worked trace.

Model

Burnside’s theorem, in the form of the anchored Lean target

Here $N_a=\{n\in N:n\cdot a=a\}$ is the stabilizer of $a$ . Normality means $gNg^{-1}=N$ for every $g\in G$ . The paper reports a completed Lean proof and reproduces the target and core-helper source; the short arguments on these pages explain selected steps, not a replacement proof of Burnside’s theorem.

\begin{gathered} |\Omega|=p\text{ prime},\quad G\leq\operatorname{Sym}(\Omega),\quad G\curvearrowright\Omega\text{ transitive},\\ \Longrightarrow\quad G\curvearrowright\Omega\text{ is 2-transitive}\quad\lor\\ \exists N\leq G : \quad N\trianglelefteq G,\quad N\curvearrowright\Omega\text{ transitive},\quad \forall a\in\Omega,\ N_a=\{1\}. \end{gathered}

MerLean-Prover, arXiv:2605.26959v2 (27 May 2026) · §3 and Appendix C, MainTheorem

Definition

Transitive, 2-transitive, and regular actions

A transitive action can move one chosen point anywhere. A 2-transitive action can move an ordered pair of distinct points anywhere. In a regular action, the element carrying one point to another is unique; equivalently, the action is transitive and every stabilizer is trivial.

\begin{aligned} \text{transitive: }&\forall a,b\in\Omega,\ \exists g\in G : \ g\cdot a=b,\\ \text{2-transitive: }&\forall a\ne b,\ c\ne d,\ \exists g\in G : \ (g\cdot a,g\cdot b)=(c,d),\\ \text{regular: }&\forall a,b\in\Omega,\ \exists!\,g\in G : \ g\cdot a=b. \end{aligned}

Why regularity identifies a cyclic group of order p

The theorem’s formal conclusion describes an action, rather than directly saying that a subgroup is cyclic of prime order. The connection is short enough to check by hand.

Lemma

A regular action identifies group elements with points

For the finite set in Burnside’s theorem, $N$ consequently has prime order and is cyclic. The bijection concerns sets; it does not give $\Omega$ a pre-existing group structure.

N\curvearrowright\Omega\text{ regular},\ |\Omega|=p\text{ prime},\ a\in\Omega \quad\Longrightarrow\quad \phi_a:N\overset{\sim}{\longrightarrow}\Omega,\quad n\longmapsto n\cdot a. \qquad |N|=|\Omega|=p.

Proof / derivation

Transitivity makes $\phi_a$ surjective. If $n\cdot a=m\cdot a$ , then $m^{-1}n$ stabilizes $a$ . A trivial stabilizer forces $m^{-1}n=1$ , hence $n=m$ , so $\phi_a$ is injective.

Thus $|N|=p$ . Any nonidentity element of $N$ has order greater than one and dividing $p$ by Lagrange’s theorem. Its order is therefore $p$ , so it generates $N$ .

Elementary explanation of the regularity conclusion in Appendix C

Last updated November 1, 2026