Method | Euled

Procedure 1. Two-ended search.

Search expands from the axioms and from the target. Each end keeps a frontier of at most 15 lemmas. The ends alternate one move each until the gap reaches 0.

g_t = \min_{u \in F_t,\; v \in B_t} d(u, v), \qquad \text{stop when } g_t = 0

Here $F_t$ is the forward frontier at round $t$ , $B_t$ the backward frontier, $d(u,v)$ the shortest implication path from $u$ to $v$ , $g_t$ the gap.

Definition 2. Middle points.

A middle point is a statement that completes the proof once proved from both sides. The search keeps 5 of them per target and each end works toward its nearest one.

M = \{ m : F \vdash m \;\wedge\; m \vdash T \}, \qquad m^{*} = \arg\min_{m \in M} \big[ d(F, m) + d(m, T) \big]

Here $M$ is the set of middle points, $F$ the forward frontier, $T$ the target, $m^{*}$ the cheapest middle point.

Definition 3. Lemma frontier.

Each end ranks candidate lemmas by coverage per cost and keeps the top 15. The ranking is recomputed after every round.

\mathrm{cpc}(\ell) = \frac{R(\ell)\, P(\ell)}{\tau(\ell)}

Here $\ell$ is a candidate lemma, $R(\ell)$ its weighted downstream reach, $P(\ell)$ the probability it is provable, $\tau(\ell)$ the tokens to prove it.

Procedure 4. Bridge finding.

From the target, ask what would need to be true for it to be true. Each answer becomes a new statement one step closer to the forward frontier.

H_0 = \{T\}, \qquad H_{k+1} = \{ h : h \Rightarrow s \text{ for some } s \in H_k \}

Here $H_k$ is the set of bridge hypotheses after $k$ backward steps, $T$ the target, $h$ a hypothesis, $s$ a statement already in $H_k$ .

Procedure 5. Cheapest question first.

Each goal gets three attempts in order of cost: disprove it, prove its double negation, prove it directly. A proof of the double negation gives the goal with Classical.choice, one of the 3 allowed axioms.

\neg\neg P \;\to\; P \quad \text{(classical)}, \qquad \text{order: } \neg P \;\prec\; \neg\neg P \;\prec\; P

Here $P$ is the goal statement, $\neg P$ its negation, and $\prec$ means "is tried before".

Definition 6. Optimal question.

The best question closes the most open goals per token. For targets it is the problem whose solution unlocks the most downstream problems. For lemmas it is the sub-lemma that closes the most subgoals.

q^{*} = \arg\max_{q} \frac{|C(q)|}{\tau(q)}

Here $q$ is a candidate question, $C(q)$ the set of open goals closed by answering $q$ , $\tau(q)$ the tokens to answer it.

Definition 7. Failure lemma bank.

Every Lean-verified sub-lemma from a failed attempt enters the bank if it is non-trivial. Its score is the number of open goals it closes.

s(\ell) = \big|\{\, g \in G_{\mathrm{open}} : \ell \text{ closes } g \,\}\big|, \qquad \mathrm{NT}(\ell) \iff \text{exact?, simp, omega, decide, grind all fail in } 10\,\mathrm{s}

Here $\ell$ is a verified sub-lemma, $G_{\mathrm{open}}$ the open goals, $s(\ell)$ the bank score, $\mathrm{NT}$ the non-trivial filter.

Definition 8. Coverage graph.

The graph joins LeanGraph (388,105 nodes, 11.3M edges) with the 909 formal-conjectures Erdős files and the 68 FME conjectures. Reach counts open nodes weighted by distance.

R(v) = \sum_{w \in O(v)} \frac{1}{d(v, w)}

Here $v$ is a node, $O(v)$ the open nodes reachable from $v$ , $d(v,w)$ the bridge distance from $v$ to $w$ , $R(v)$ the weighted downstream reach.

Definition 9. AI-rated hypotheses.

A model rates which bridge hypotheses and middle points to try. The rating combines four inputs.

\rho(h) = f\big( p(h),\; d_F(h),\; d_B(h),\; n(h) \big)

Here $h$ is a hypothesis, $p$ the estimated provability, $d_F$ and $d_B$ the distances to the forward and backward frontiers, $n$ the concept novelty, $f$ the combining function fitted on past success.

Procedure 10. Shortener cascade.

Five steps shorten a verified proof. Every step must Lean-verify. Steps 1 to 3 run twice on CPU as an idempotence test: a second pass that shortens again is a defect in the first.

\mathrm{red}(\pi) = 1 - \frac{|\pi_{5}|}{|\pi_{0}|}, \qquad |\pi_{i+1}| = |\pi_i| \text{ on a second pass}

Here $\pi_0$ is the input proof, $\pi_i$ the proof after step $i$ , $|\pi|$ its step count, $\mathrm{red}$ the reduction.

Procedure 11. Physarum shortest path.

Conductivity on each implication edge grows with the flow it carries and decays otherwise. Edges on short bridges end with high conductivity. The method keeps several parallel paths and adapts as the bank grows.

Q_e = \frac{D_e}{L_e}\,(p_i - p_j), \qquad \frac{dD_e}{dt} = |Q_e| - D_e

Here $e=(i,j)$ is an edge, $D_e$ its conductivity, $L_e$ its length, $p_i$ and $p_j$ the pressures at its ends, $Q_e$ the flow.

Definition 12. One shared engine.

One function scores targets, scores lemmas, and defines the objective that Optuna maximizes in C4. The optimizer and the system therefore rank by the same quantity.

\mathrm{cpc} = \frac{R \cdot P}{\tau}, \qquad J = \frac{N_{\mathrm{nt}}}{t_{\mathrm{cpu}}}

Here $R$ is weighted downstream reach, $P$ the probability of being provable, $\tau$ the tokens, $J$ the C4 objective, $N_{\mathrm{nt}}$ the non-trivial verified solves on the held-out PutnamBench slice, $t_{\mathrm{cpu}}$ the CPU-minutes.