MerLean-Prover · Chapter 02

A proof plan that can be revised

The shared object is a dependency graph of mathematical statements. Planning edits that graph, Lean implements a statement, and independent checks decide what should happen next.

Local proof obligations, explicit dependencies

Each node stores a statement, an informal proof sketch, its prerequisites, and a completion status. Helpers are processed before the statements that use them. The target node also stores the original declaration as its anchor.

Planning may revise the decomposition; Lean may write and repair code; a fresh Check invocation answers one question. After a plan revision, dependent statements must be reconsidered rather than inheriting an obsolete success status.

Definition

A dependency graph and its affected statements

Arrows point from a statement to a helper it needs. A path $v\leadsto u$ means that $v$ depends on $u$ , possibly through intermediate lemmas. A change to $u$ invalidates affected dependent statements. This notation describes the paper’s dependency discipline; it is not a new convergence guarantee.

\begin{aligned} D&=(V,E),\qquad (v,u)\in E\ \Longleftrightarrow\ T_v\text{ uses }T_u,\\ \operatorname{Affected}(u)&=\{v\in V : \ v\leadsto u\}\cup\{u\}. \end{aligned}

MerLean-Prover, arXiv:2605.26959v2 (27 May 2026) · §2, shared proof plan

Faithfulness: does a clean-build result still prove the intended statement?
Math: is a stuck statement correct under its stated hypotheses?
Decomposition: should a mathematically sound but difficult obligation be split into smaller ones?

MerLean-Prover architecture: a shared proof plan connects Planning, Lean, and Check agents through compilation, faithfulness, mathematical correctness, and decomposition decisions. — The paper’s architecture diagram. Each invocation has one objective; failed checks can revise the shared plan, while a successful exit requires closure of the original target. This is an architecture diagram, not a benchmark trace.

From a prime-order element to a normal subgroup

In the non-2-transitive branch, the public proof chooses an element $\tau\in G$ of order $p$ and sets $N=\langle\tau\rangle$ . Separate helpers establish that this subgroup acts regularly and that conjugating $\tau$ by any $g\in G$ stays in $N$ . The latter step uses the Müller affine-conjugation result in the recorded plan.

The normality argument below shows how a substantial imported lemma and a short algebraic deduction fit together. The affine-conjugation hypothesis carries the hard part; the calculation does not prove that hypothesis.

Lemma

It suffices to control conjugation of a generator

This elementary implication is the normality step used by the closed BurnsideDichotomyCore proof. It applies to any group $G$ and element $\tau$ once the displayed conjugation hypothesis is available.

N=\langle\tau\rangle,\qquad \forall g\in G,\ g\tau g^{-1}\in N \quad\Longrightarrow\quad N\trianglelefteq G.

Proof / derivation

Every element of $N$ is $\tau^k$ for some integer $k$ . Conjugation respects integer powers, and a subgroup is closed under those powers, so the displayed identity gives $gNg^{-1}\subseteq N$ .

Apply the same inclusion to $g^{-1}$ to obtain $g^{-1}Ng\subseteq N$ . Conjugating it by $g$ gives $N\subseteq gNg^{-1}$ . The two inclusions prove normality.

g\tau^kg^{-1}=(g\tau g^{-1})^k\in N\qquad(k\in\mathbb Z).

MerLean-Prover, arXiv:2605.26959v2 (27 May 2026) · Appendix C, cyclicSubgroup_normal

Follow the published Burnside proof plan

The recorded run starts with six nodes: the target and five helpers. A helper passes compilation but fails the Faithfulness check, so the plan is repaired. Later, exhausted proof attempts trigger new decompositions, and a Math check catches a helper missing a necessary hypothesis.

The plan expands through 12 and 21 nodes to 32. Its node set stabilizes by frame 51, and the original target closes at frame 63. The replay below pairs documented milestones with selected neighborhoods of the final published dependency graph. It does not reconstruct the graph at each frame or run a live Lean session.

Anchored target

Burnside's prime-degree theorem

Let G ≤ Sym(Ω) act transitively on a finite set Ω with |Ω| = p prime. Then G is 2-transitive, or there exists N ◁ G acting regularly on Ω. Regular means transitive with trivial point stabilizers: Stab_N(x) = {1} for every x ∈ Ω.

Read the target in Lean

import Mathlib.GroupTheory.GroupAction.MultipleTransitivity
import FormalQualBench.BurnsidePrimeDegreeTheorem.Auxiliary.BurnsideDichotomyCore

namespace BurnsidePrimeDegreeTheorem
open MulAction

theorem MainTheorem
    {α : Type*} [Fintype α]
    {G : Subgroup (Equiv.Perm α)}
    (htrans : IsPretransitive G α)
    (hp : (Fintype.card α).Prime) :
    IsMultiplyPretransitive G α 2 ∨
      ∃ N : Subgroup G, N.Normal ∧ IsPretransitive N α ∧
        ∀ a : α, MulAction.stabilizer N a = ⊥ := by
  classical
  rcases Classical.em (IsMultiplyPretransitive G α 2) with h2 | hNot2
  · exact Or.inl h2
  · haveI : IsPretransitive G α := htrans
    exact Or.inr (burnside_dichotomy_core hp hNot2)

end BurnsidePrimeDegreeTheorem

Documented milestone

01 / 06Frame 0

Start with six statements

The first plan has the anchored theorem #1 and five prerequisites #2–#6. Four prerequisites are subsequently closed, leaving the dichotomy core #2 as the hard step.

Final published plan

A dependency neighborhood

Inspect a node

Mentioned in this milestoneArrows: claim → prerequisite

An arrow A → B means statement A uses prerequisite B in the final displayed graph. It does not indicate execution order or when that dependency was added. Milestones change the highlight, not the graph. Scroll across the diagram on small screens.

Node 1First recorded: frame 0

Burnside's prime-degree theorem

Thm_MainTheorem

The anchored target. Appendix C records its closure at frame 63; its proof handles the 2-transitive case immediately and delegates the other case to node #2.

Plan-level prerequisites

Inspect the published Lean excerpt

import Mathlib.GroupTheory.GroupAction.MultipleTransitivity
import FormalQualBench.BurnsidePrimeDegreeTheorem.Auxiliary.BurnsideDichotomyCore

namespace BurnsidePrimeDegreeTheorem
open MulAction

theorem MainTheorem
    {α : Type*} [Fintype α]
    {G : Subgroup (Equiv.Perm α)}
    (htrans : IsPretransitive G α)
    (hp : (Fintype.card α).Prime) :
    IsMultiplyPretransitive G α 2 ∨
      ∃ N : Subgroup G, N.Normal ∧ IsPretransitive N α ∧
        ∀ a : α, MulAction.stabilizer N a = ⊥ := by
  classical
  rcases Classical.em (IsMultiplyPretransitive G α 2) with h2 | hNot2
  · exact Or.inl h2
  · haveI : IsPretransitive G α := htrans
    exact Or.inr (burnside_dichotomy_core hp hNot2)

end BurnsidePrimeDegreeTheorem

Browse all 32 nodes in the published plan

What the final check certifies

The agent checks guide search; they are not substitutes for Lean’s kernel. The benchmark accepts a solve only after the plan closes, the original target signature is preserved, the project builds, and the target’s transitive axiom dependencies pass the audit.

The audit follows dependencies, so moving an unproved claim into a helper does not hide it. The permitted standard axioms are made explicit below; this is not a claim that the proof uses no axioms whatsoever.

Model

The reported axiom policy

The paper uses a transitive #print axioms audit. It excludes unfinished placeholders and user-introduced axioms from the proof closure. The original Lean signature is checked separately; natural-language-to-Lean conversion is outside this evaluation.

\begin{gathered} \operatorname{Axioms}(p)\subseteq \{\mathtt{propext},\ \mathtt{Quot.sound},\ \mathtt{Classical.choice}\},\\ \mathtt{sorryAx}\notin\operatorname{Axioms}(p). \end{gathered}

MerLean-Prover, arXiv:2605.26959v2 (27 May 2026) · §§2, 4

Last updated November 1, 2026