\documentclass{article} % For LaTeX2e \usepackage{iclr2027_conference,times} % Optional math commands from https://github.com/goodfeli/dlbook_notation. \input{math_commands.tex} \usepackage{hyperref} \usepackage{url} \usepackage{graphicx} \usepackage{wrapfig} \usepackage{needspace} \usepackage{algorithm} \usepackage{algpseudocode} \usepackage{xcolor} \usepackage{tikz} \usetikzlibrary{positioning,arrows.meta,calc} \AddToHook{env/table/begin}{\renewcommand{\arraystretch}{1.25}} \newif\ifshowcomments \showcommentstrue \newcommand{\aacomment}[1]{\ifshowcomments\textcolor{red}{\textbf{AA:} #1}\fi} \title{Automated Conjecturing: \\ Generation, Selection and Evaluation} \author{ \textbf{Ayush Agrawal$^{1,2,3\dagger}$, Vedant Shah$^{1,2}$, Navin Goyal$^{3*}$, Ankit Anand$^{1,4*}$, Aaron Courville$^{1,2*}$} \\[0.4em] {\small $^1$MILA - Quebec AI Institute,\quad $^2$Universit\'e de Montr\'eal,\quad $^3$Microsoft Research,\quad $^4$McGill University} \\[0.4em] {\small $^*$Equal advising.\quad $^\dagger$Correspondence to Ayush Agrawal: \hypersetup{hidelinks}\href{mailto:ayushagrawal1801@gmail.com}{ayushagrawal1801@gmail.com}} } \iclrfinalcopy \begin{document} \maketitle \lhead{Preprint} \begin{abstract} Deciding which conjectures are worth proving is a crucial part of mathematical discovery, and a system that learns mathematics from its axioms alone must make that decision without human guidance. Self-play provers such as Minimo learn a conjecturer alongside the prover and reward it for producing hard conjectures, but a conjecture that is harder to prove is not necessarily more useful for improving a prover: the learned conjecturer drifts toward long, artificial statements. We study conjecturing in a controlled, single-round setting in the Peano formal environment, across propositional logic, abelian groups, and natural-number multiplication, evaluating a set of conjectures by how much a fixed prover improves on held-out theorems after training on their proofs. We show that a far simpler generator does better: making small structural edits to statements the prover already knows yields conjectures that, at an equal training budget and under best-first search, improve the prover by 6 to 13 percentage points more than Minimo's learned conjectures. The gain holds even when conjectures are drawn at random from the generated pool. In contrast to the common practice of selecting the most difficult statements, we also propose Hard Neighbours (HN), a score that favors conjectures whose proof difficulty grows disproportionately relative to their structural distance from easier reference statements; HN gives the largest selection gains in propositional logic, but no selection method is best in every domain. In the current setting, how conjectures are generated matters more than how they are selected, and structural perturbation is the baseline that future conjecturers should be measured against. Apart from improvements in proving ability, we also study other attributes of generated proofs: the amount of search required and the length of the proofs. \end{abstract} \section{Introduction} \label{sec:introduction} AI systems have advanced rapidly at the frontiers of mathematics, with recent developments including OpenAI's announcement of a proposed solution to the Navier-Stokes Millennium Prize problem~\citep{openai-finite-time-blowup}. However, mathematical discovery is not only about proving open problems; it is also about posing new ones. Therefore, autonomous mathematical discovery requires systems that can generate conjectures worth working on. Conjecturing is a crucial part of mathematical discovery: Fermat's last theorem, the Riemann hypothesis, and Goldbach's conjecture each began as a judgment that a statement was worth pursuing, and shaped mathematics long before any proof appeared. A system that learns mathematics from its axioms alone must make such judgments itself, proposing statements and deciding which are worth the effort of proving; this is what separates a prover from a discoverer. Formal mathematics is the right test bed for this capability, because every statement and proof can be checked mechanically, so progress is measurable without human judgment in the loop. Recent self-play systems learn to conjecture and prove together, using the prover's performance to guide subsequent conjecture generation~\citep{poesia2024minimo,dong2025stpselfplayllmtheorem}. Their objective is to generate statements that are hard but still provable for the current prover. As the prover improves, the conjecturer is encouraged to propose increasingly harder problems. However, this objective leads to undesirable outcomes. Minimo~\citep{poesia2024minimo}, one of such setups, mentions that conjecturer collapses into making longer and more complicated statements with almost no mathematical value. Similarly, STP~\citep{dong2025stpselfplayllmtheorem} reports mode collapse toward algebraic manipulations and introduces both a diversity mechanism and a filter against artificially complicated goals. These observations expose a limitation of difficulty as a selection signal: making a statement harder for a prover does not necessarily make it more useful or interesting. \begin{figure}[!t] \centering \resizebox{\textwidth}{!}{% \begin{tikzpicture}[ node distance=12mm, stage/.style={draw=black!70, fill=blue!4, rounded corners=2pt, align=center, font=\small, inner sep=5pt, minimum height=11mm}, qlabel/.style={font=\small\bfseries, align=center}, vary/.style={font=\scriptsize, align=center, text=black!75}, finding/.style={font=\scriptsize\itshape, align=center, text=blue!45!black}, arr/.style={-{Stealth[length=2.2mm]}, thick, black!70}, ] % ---- pipeline boxes ---- \node[stage] (seeds) {Known statements\\[-1pt]{\scriptsize (domain axioms)}}; \node[stage, right=of seeds] (pool) {Candidate pool\\[-1pt]{\scriptsize proved in Peano}}; \node[stage, right=of pool] (train) {Training proofs\\[-1pt]{\scriptsize matched example budget}}; \node[stage, right=of train] (eval) {Prover\\[-1pt]improvement}; \draw[arr] (seeds) -- (pool); \draw[arr] (pool) -- (train); \draw[arr] (train) -- (eval); % ---- stage labels above arrows ---- \node[qlabel, above=1.5mm of $(seeds.north east)!0.5!(pool.north west)$] {1.~Generation}; \node[qlabel, above=1.5mm of $(pool.north east)!0.5!(train.north west)$] {2.~Selection}; \node[qlabel, above=1.5mm of $(train.north east)!0.5!(eval.north west)$] {3.~Evaluation}; % ---- what we vary ---- \node[vary, below=5mm of $(seeds.south east)!0.5!(pool.south west)$] (v1) {structural perturbations\\vs.\ learned conjecturer}; \node[vary, below=5mm of $(pool.south east)!0.5!(train.south west)$] (v2) {Hard Neighbours vs.\ random,\\hardness, length heuristics}; \node[vary, below=5mm of $(train.south east)!0.5!(eval.south west)$] (v3) {BFS \& rollouts over graded benchmarks}; % ---- row labels ---- \node[vary, left=2mm of v1.west, anchor=east, text=black!55] {\emph{we compare:}}; \end{tikzpicture}} \caption{The three design decisions in an automated conjecturing pipeline.} \vspace{-13pt} \label{fig:overview} \end{figure} Consider a scenario where a high-school student has learned that $x^2-1=(x-1)(x+1)$. What should they practice next in order to improve their understanding of the area? One could ask them to factor $4x^2-4$, which repeats the same identity with a constant factor, or $x^3-1$, which introduces a different factorization. Once they have practiced, how would one know whether the student has made progress? This presents three separate decisions. First, one must produce candidate exercises. Second, one must choose which exercises to assign. Third, one must assess whether practicing them helped the student solve other problems. We work in a theorem proving setup where our prover faces the same questions: where should its conjectures come from, out of them, which should it learn from, and how to measure its progress? This motivates examining the three design choices for automated conjecturing: how candidate statements are \emph{generated}, which of them are \emph{selected} for the prover to learn from, and how we \emph{evaluate} the progress (Figure~\ref{fig:overview}). When generation and selection change together within a training loop, improvements in prover performance do not reveal which component was responsible. Conversely, increasing conjecture difficulty does not establish that the resulting training data is better for improving the prover. We therefore compare candidate sources and selection methods within a fixed pool, with base prover’s improvement as our primary method of evaluation. We work in a small, controlled setting: the Peano formal theorem proving environment~\citep{poesia2023peano}, which enumerates legal actions at each proof state. Within this environment, we explore three distinct domains: propositional logic, natural-number multiplication, and abelian groups. Each training comparison starts from the same randomly initialized 25M parameter transformer model~\citep{vaswani2017attention} (acting as a prover) and uses a single round of selection and finetuning. Our primary criterion is prover’s improvement on difficulty-graded benchmarks after training on the selected proof traces, with matched training data samples. We evaluate using policy-guided best-first search (BFS) and policy rollouts, neither requiring a separately trained value function. This scale allows us to vary the design choices, and inspect generated statements and proofs. Our candidate generator and selection score share a motivation: small changes to a known statement can produce a substantially more difficult candidates that could be of interest. For example, replacing one occurrence of $A$ by $B$ in the intuitionistically provable $((A\to A)\to A)\to A$ yields Peirce's law, $((A\to B)\to A)\to A$, which can be proven only in classical logic. The statement ``every even integer greater than two is the sum of two positive integers'' is trivial. Replace ``positive integers'' with ``prime numbers'', and we obtain Goldbach's conjecture: a small change turns a trivial observation into a much harder and genuinely interesting mathematical statement. Since the candidates are closer to the known statements, they are more likely to be hard for interesting reasons. These examples motivate both our generator and our selection score. We generate candidates by \emph{structural perturbation}, editing the abstract syntax tree of a known statement, so that every candidate is a small edit away from something already proved (see Figure~\ref{fig:perturbation}). We then select the candidates for which that small edit produced a large jump in proof-search effort. The \emph{Hard Neighbours} (HN) score measures this jump relative to the edit distance from easier reference statements. As baselines we use random selection, absolute hardness, hardness per token, and shortest statements. Across the three domains, our comparisons yield three findings. First, the generation method has a large effect on the prover's improvement on the set benchmarks. Finetuning on proof traces from HN-selected perturbed statements outperforms finetuning on Minimo-generated statements in all three domains under best-first search, by 7 to 13 percentage points; random selection from the same pool is a competitive baseline, already improving over Minimo by 6 to 9 points (see Table~\ref{tab:overall-solve-summary}). The advantage extends to benchmark levels where Minimo-trained provers solve no problems. This finding also holds under rollout evaluation in logic and groups, while Minimo achieves a slightly higher peak solve rate in natural-number multiplication. Second, selection yields additional training gains in logic and groups, but no criterion consistently improves both peak solve rate and coverage over random selection across all three domains. Selecting the hardest provable conjectures is not the strongest criterion in any domain under BFS. In a separate experiment, we inject benchmark theorems into the candidate pool and measure whether they are selected by the scorers. HN exceeds the random selection in all three domains, but selecting shortest statements is competitive in logic and arithmetic and selects the most benchmark theorems in groups. Third, evaluation choices affect the conclusions. A checkpoint's solve rate can decline while coverage across checkpoints continues to grow. Search also affects the returned proof quality: on matched solved subsets, rollout proofs are around two times as long as BFS proofs on average, and a concrete example contains repeated steps that leave the proof obligation unchanged (Table~\ref{tab:contraposition-traces} in Appendix~\ref{app:proof-lengths}). Our contributions are: (1) A single-round study in Peano environment that examines conjecture generation, selection, and evaluation using approximately matched training samples. (Sections~\ref{sec:methods}--\ref{sec:evaluation}). (2) A structural-perturbation generator requiring no learned generation model, and the finding that its proved candidates provide better training signal than the Minimo pool under BFS in all three domains (Section~\ref{sec:results}). (3) The Hard Neighbours (HN) selection score, which combines structural similarity with relative proof-search difficulty to select prover-training data. HN gives the largest selection gains in propositional logic where it exceeds Random by around 5 percentage points of peak solve rate and 7.5 percentage points of coverage, though no selection method improves consistently across all three domains (Section~\ref{sec:results}). (4) Difficulty-graded benchmarks for three formal domains and an analysis of how search procedure and evaluation measure affect the conclusions (Sections~\ref{sec:evaluation}--\ref{sec:results}). \section{Related Work} \label{sec:related-work} \begin{figure}[!t] \centering \resizebox{0.7\textwidth}{!}{% \begin{tikzpicture}[x=1cm,y=1cm,>=Stealth, stmt/.style={font=\small}, tnode/.style={font=\small, inner sep=1.5pt}, note/.style={font=\small, text=black!60, align=center}, dom/.style={font=\small\bfseries, text=black!75}, swap/.style={<->, thick, orange!80!black, bend right=50}, ] % ---- propositional logic ---- \begin{scope}[shift={(0,0)}] \node[dom] at (1.6,2.35) {Propositional logic}; \node[stmt] at (1.6,1.7) {$(A\land B)\to(A\land B)$}; \node[tnode] (r) at (1.6,0.95) {$\to$}; \node[tnode] (h) at (0.7,0.25) {$A\land B$}; \node[tnode] (c) at (2.5,0.25) {$\land$}; \node[tnode, text=blue!70!black] (l1) at (2.0,-0.5) {$A$}; \node[tnode, text=green!40!black] (l2) at (3.0,-0.5) {$B$}; \draw (r)--(h); \draw (r)--(c); \draw (c)--(l1); \draw (c)--(l2); \draw[swap] (l1.south) to (l2.south); \node[stmt] at (1.6,-1.55) {$(A\land B)\to({\color{green!40!black}B}\land{\color{blue!70!black}A})$}; % \node[note] at (1.6,-2.2) {a trivial identity becomes\\conjunction commutativity}; \end{scope} % ---- natural-number multiplication ---- \begin{scope}[shift={(5.35,0)}] \node[dom] at (1.6,2.35) {Natural-number multiplication}; \node[stmt] at (1.6,1.7) {$a\times 0=0$}; \node[tnode] (r) at (1.6,0.95) {$=$}; \node[tnode] (m) at (0.85,0.25) {$\times$}; \node[tnode] (z2) at (2.35,0.25) {$0$}; \node[tnode, text=blue!70!black] (l1) at (0.35,-0.5) {$a$}; \node[tnode, text=green!40!black] (l2) at (1.35,-0.5) {$0$}; \draw (r)--(m); \draw (r)--(z2); \draw (m)--(l1); \draw (m)--(l2); \draw[swap] (l1.south) to (l2.south); \node[stmt] at (1.6,-1.55) {${\color{green!40!black}0}\times{\color{blue!70!black}a}=0$}; %\node[note] at (1.6,-2.2) {an axiom becomes a new candidate}; \end{scope} % ---- abelian groups ---- \begin{scope}[shift={(10.7,0)}] \node[dom] at (1.6,2.35) {Abelian groups}; \node[stmt] at (1.6,1.7) {$a^{-1}\cdot a=e$}; \node[tnode] (r) at (1.6,0.95) {$=$}; \node[tnode] (m) at (0.85,0.25) {$\cdot$}; \node[tnode] (e2) at (2.35,0.25) {$e$}; \node[tnode, text=blue!70!black] (l1) at (0.35,-0.5) {$a^{-1}$}; \node[tnode, text=green!40!black] (l2) at (1.35,-0.5) {$a$}; \draw (r)--(m); \draw (r)--(e2); \draw (m)--(l1); \draw (m)--(l2); \draw[swap] (l1.south) to (l2.south); \node[stmt] at (1.6,-1.55) {${\color{green!40!black}a}\cdot{\color{blue!70!black}a^{-1}}=e$}; %\node[note] at (1.6,-2.2) {an axiom becomes a new candidate}; \end{scope} \draw[black!20] (4.55,2.5) -- (4.55,-2.5); \draw[black!20] (9.9,2.5) -- (9.9,-2.5); \end{tikzpicture}} \caption{One perturbation across three domains: swapping two arguments in a statement's abstract syntax tree yields a new candidate statement. Colors track the swapped subterms. These are simple syntactic edits that need not preserve truth or increase difficulty; Appendix~\ref{app:perturbation-operations} lists all perturbations we did per domain.} \vspace{-0.5cm} \label{fig:perturbation} \end{figure} Computer programs that propose mathematical statements date to AM, Graffiti, and HR~\citep{lenat11984automated,graffiti,colton2001automated}, followed by theory exploration~\citep{johansson2011conjecture} and recently, by LLM based systems that evolve mathematical constructions using search~\citep{novikov2025alphaevolve}, mine literature for finding problems to solve~\citep{zheng2026problemproblemscalablemathematical}. Closest to our work are systems that generate statements to train provers: learned theorem generators~\citep{wang2020learning}, synthetic data at scale~\citep{trinh2024solving} and self play systems that couple the conjecturer and the prover such as Minimo~\citep{poesia2024minimo}, STP~\citep{dong2025stpselfplayllmtheorem} or as as self-generated curriculum~\citep{bailey2026scalingselfplayselfguidance}. These systems typically reward conjectures for being hard but provable, and this difficulty based reward is hackable: conjectures drift towards longer and artificially complex statements. Moreover, generation, selection and evaluation are entangled where gains are hard to attribute to any single component. We study each stage of generation, selection and evaluation in the small scale setup, Peano~\citep{poesia2023peano} and ask whether a learned conjecturer beats a simple perturbation based generation baseline at matched training budget. Similarly, to avoid selecting complex statements, we use a selection score that selects candidates that are structurally close to the starting known statements but relatively harder to prove and compare with selection based on absolute hardness, and examine how the conclusions depend on the evaluation procedures as well. \begin{figure}[!t] \centering \setlength{\abovecaptionskip}{2pt} \includegraphics[width=\linewidth]{figures/generation_bfs_curves.pdf} \par\nointerlineskip \caption{Training on samples from perturbation-based conjecturer yields higher BFS solve rates than training on Minimo-generated conjectures at every evaluated checkpoint in all three domains. Minimo's solve rate declines after epoch~30 in logic and epoch~60 in groups, while its coverage continues to rise: later checkpoints solve new problems while losing some previously solved ones. Blue curves show the perturbation-based conjecturer with HN selection. Dashed curves show solve rate; solid curves with circles show coverage. Shading denotes $\pm1$ sample SD across three seeds; solid gray lines show the starting prover's performance.} \label{fig:generation-comparison} \end{figure} \section{Background: The Peano Environment} \label{sec:background} We work in Peano~\citep{poesia2023peano}, a formal theorem proving environment. We consider three domains: propositional logic, natural-number multiplication, and abelian groups. Each domain is specified by a set of axioms and inference rules, listed in Appendix~\ref{app:domain-axioms}. These domains expose different reasoning requirements, including logical rule composition and case analysis, equality rewriting, and induction. A proof state contains a goal and its local context. Peano enumerates the legal actions available in that state and computes the states resulting from their execution. In order to arrive at the proof, a learned policy has to select the right actions given the state until all proof states are closed. \paragraph{Example.} Consider proving that conjunction is commutative. The statement is written Peano as \begin{center} \small\texttt{[('A : prop) -> ('B : prop) -> (and 'A 'B) -> (and 'B 'A)]} \end{center} A proof is a sequence of actions. After three introduction actions bind $A$, $B$, and the assumption $h:A\land B$, Peano enumerates the legal next steps: five in this state, such as extracting either conjunct of $h$ or splitting the goal, and the policy chooses among them. Extracting $A$ and $B$ from $h$ and then applying conjunction introduction closes the goal, for a total of nine actions. Each proof state paired with its chosen action is one policy training example, and the number of partial proofs a search expands before finding a proof is our measure of the statement's cost for the prover (Section~\ref{sec:methods-search}). Appendix~\ref{app:conjunction-proof} gives the full proof and its nine recorded actions. \paragraph{Prover} The prover is a randomly initialised 25M-parameter transformer following~\citet{poesia2024minimo}. Peano enumerates the legal actions at each proof state, and the model scores each state-action pair. During training, actions taken in recorded proofs receive label Y, while the other legal actions receive label N. At search time, we use the model's predicted probability of Y, normalized over its Y and N predictions, as the action's score, and normalize these scores across the legal actions to obtain the distribution used by proof search (Appendix~\ref{app:policy-scoring}). \paragraph{Best-first search.} \label{sec:methods-search} Policy-guided best-first search (BFS) prioritizes partial proofs by their cumulative log-probability, following GPT-f~\citep{polu2020generativelanguagemodelingautomated}. It maintains a priority queue of partial proofs; at each iteration it removes the highest-priority partial proof, explores its legal next actions, and adds the resulting unfinished proofs to the queue. We measure \emph{search effort} by the number of partial proofs removed from the queue for expansion, or \emph{queue removals}; the search budget limits this count. Search effort differs from \emph{proof length}, which counts the actions in the returned proof. We use BFS without a learned value function so that differences in proving performance can be attributed to the training data rather than to the value model or search hyperparameters, as in MCTS-style provers~\citep{lample2022hypertreeproofsearchneural,poesia2024minimo}. Algorithm~\ref{alg:bestfirst} in Appendix~\ref{app:bestfirst-search} gives the full procedure. \paragraph{Policy rollouts.} \label{sec:methods-rollouts} As a second search procedure, policy rollout search (Algorithm~\ref{alg:rollout} in Appendix~\ref{app:rollout-search}) follows a single proof trajectory per attempt, choosing one legal action at a time for the leftmost open subgoal. Unlike BFS, it maintains no frontier of alternative paths and does not backtrack within an attempt. A greedy attempt always chooses the highest-scoring action; if it fails, subsequent attempts restart from the original statement and sample actions from the policy distribution. \paragraph{Minimo as a learned conjecturer.} Our learned-generation baseline is the Minimo conjecturer~\citep{poesia2024minimo}, which learns to conjecture and prove through an iterative self-play loop in Peano, starting from randomly initialized parameters: the conjecturer generates well-formed statements through constrained decoding and type-directed synthesis, and learns to target hard but provable conjectures from proof-search feedback. \begin{figure}[!t] \centering \setlength{\abovecaptionskip}{2pt} \includegraphics[width=0.8\linewidth,trim=0 6bp 0 0,clip]{figures/bfs_paired_bars.pdf} \par\nointerlineskip \caption{Selection gains vary by domain under best-first search at a 4,000-removal budget. Selection helps most in logic, where HN improves on Random by about 5 percentage points in peak solve rate and 8 points in coverage. In groups, Hard/length leads, exceeding Random's peak solve rate by about 3 points; in natural-number multiplication, no method exceeds Random's peak. Each pair shows peak solve rate (dark, left) and coverage (light, right) (Section~\ref{sec:evaluation-metrics})} \vspace{-10pt} \label{fig:selection-comparison} \end{figure} \section{Conjecture Generation} \label{sec:methods-generation} \label{sec:evaluation-pools} \label{sec:methods} \label{sec:methods-perturbation} \paragraph{Generation by Structural Perturbation.} We generate candidates by editing the abstract syntax trees (ASTs) of seed statements, without training a conjecture generator. Appendix~\ref{app:generation-seeds} lists the initial seeds for each domain. Each edit changes a selected subexpression or its variables. Figure~\ref{fig:perturbation} illustrates the idea across the three domains. In propositional logic, for example, exchanging the conjuncts in the conclusion of $(A\land B)\to(A\land B)$ produces $(A\land B)\to(B\land A)$. The operations include replacing or exchanging variables, introducing a fresh variable, changing an operator, adding or removing a unary operation, and inserting, removing, or replacing subexpressions. We instantiate these operations with the vocabulary of each domain: logical connectives and negation in propositional logic; addition, multiplication, and successor in arithmetic; and multiplication and inverse in groups. For the equational domains, edits can also add or remove equality hypotheses. These are candidate-generating operations, not inference rules: they need not preserve truth. For example, replacing conjunction by disjunction in $(A\land B)\to A$ produces $(A\lor B)\to A$, which is false. Appendix~\ref{app:perturbation-operations} specifies the operations for each domain. For each domain, we start with easiest set of problems (axioms) and then apply these edits to form more statements. The new statements become seeds and then this process is repeated for five times. \paragraph{Generation by a learned conjecturer.} Our learned-generation baseline uses the Minimo conjecturer introduced in Section~\ref{sec:background}. We collect candidates from Minimo across its five training iterations. \paragraph{Filtering} Candidates from either source are deduplicated, checked for well-formedness in Peano, and we simply discard candidates refuted by an oracle (Z3~\citep{demoura2008z3} for logic and multiplication, finite-model counterexample search for groups). The surviving candidates are then submitted to proof search, and only those statements that can be proved by base model are passed to next stage of conjecture selection. (Section~\ref{sec:methods-selection}). Appendix~\ref{app:generation-details} gives the pool construction details and sizes. \section{Conjecture Selection} \label{sec:methods-selection} Given a large list of candidate conjectures which can be proved by a base model, it is unclear if all candidates are equally interesting and informative to selected as ``conjectures" and can aid further in development of stronger provers. Recent work often favors statements that are hard but still provable for the current prover \citep{poesia2024minimo,dong2025stpselfplayllmtheorem}. However, selecting conjectures by hardness alone is weak as it can favor long, mechanical statements, which may have little learning utility. To address this, we develop a novel notion of hardness, called as \emph{Hard Neighbors} which brings out the concept of hardness relative to some reference statements. The idea of Hard Neighbours (HN), is to reward those difficult statements which are structurally and syntactically similar to easier reference statements(Figure~\ref{fig:hn-intuition}) but are themselves very hard, i.e they require disproportionate search effort compared to reference statements. We further compare this selection strategy with the notions popular in literature like selecting shorter statements only, selecting hard statements only as well as selecting statements randomly out of generated pool. \begin{wrapfigure}{r}{0.52\textwidth} \centering \resizebox{\linewidth}{!}{% \begin{tikzpicture}[>=Stealth, font=\scriptsize, stmt/.style={draw=black!60, rounded corners=2pt, inner sep=2.5pt, align=center}, note/.style={font=\tiny, text=black!60}, ray/.style={->, black!55, thick}, dlab/.style={fill=white, inner sep=1pt, font=\tiny, text=black!60}, ] \node[stmt, fill=blue!6] (r) at (0,0) {$((A\to A)\to A)\to A$\\[-1pt] {\tiny reference $r$ (easy)}}; \node[stmt, fill=red!55, text=white, draw=black, line width=1.1pt, above=6mm of r] (nh) {$((A\to \mathbf{B})\to A)\to A$\\[-1pt] {\tiny Peirce's law}\\[-1pt] {\tiny\bfseries selected: small edit, high search cost}}; \node[stmt, fill=blue!6, below=6mm of r] (ne) {$((A\to A)\to \mathbf{B})\to B$\\[-1pt] {\tiny still trivial}\\[-1pt] {\tiny not selected: small edit, low search cost}}; \node[stmt, fill=red!55, text=white, right=9mm of r] (fh) {$(A\land A)\to(A\lor A)\to$\\[-1pt] $\neg\neg(B\land B)\to B$\\[-1pt] {\tiny long, mechanical}\\[-1pt] {\tiny not selected: many edits away, high search cost}}; \draw[ray] (r) -- (nh) node[dlab, midway] {$d=1$}; \draw[ray] (r) -- (ne) node[dlab, midway] {$d=1$}; \draw[ray] (r) -- (fh) node[dlab, midway] {$d\gg1$}; \end{tikzpicture}% } \caption{Hard Neighbours: small structural changes can produce large jumps in proof-search difficulty. Red marks costly statements; the thick border marks the HN selection.} \vspace{-10pt} \label{fig:hn-intuition} \end{wrapfigure} \paragraph{Hard Neighbours (HN).} Given a large set of statements from the perturbation pipeline, (from section \ref{sec:methods-perturbation}, the goal of selection strategy is to determine the most useful conjectures for prover's improvement, out of this vast pool. For each candidate $c$, we perform the best first search and collect its proof (we have the proof for all candidates because we filter the candidates which can be proven by the base prover in the previous step). As a proxy for search effort, we define hardness (denoted as $b(c)$) as the number of queue removals used to prove the conjecture $c$. We further define log-hardness as $h(c)=\log(1+b(c))$. We also define a distance metric which captures syntactic difference between any two statments. Let $d(a,b)$ be the Levenshtein distance between the token sequences of statements $a$ and $b$, using unit-cost insertions, deletions, and substitutions. Lastly, a reference set is used to compute the utility or value of each candidate $c$. We initialize this reference set with domain's available proved axiom level statements at round t=0 and each subsequent round builds a new reference set as described below. At selection round $t$, let $R_t$ be the reference set and $R_t^{<}(c)=\{r\in R_t:b(r) A: ??? \end{verbatim} The proof state contains the local context and current goal. During training, this input is followed by Y for the action taken in the recorded proof, or N for another legal action. Let $z_Y(s,a)$ and $z_N(s,a)$ denote the model's next-character logits for these two labels. We compute an action score \[ q(s,a)= \frac{\exp(z_Y(s,a))} {\exp(z_Y(s,a))+\exp(z_N(s,a))}. \] We then normalize across the legal actions $\mathcal{A}(s)$: \[ \pi(a\mid s)= \frac{q(s,a)}{\sum_{a'\in\mathcal{A}(s)}q(s,a')}. \] Greedy rollouts choose the action with the largest probability, while sampled rollouts draw from this distribution at temperature 1. BFS assigns each partial proof the cumulative priority \[ g=\sum_t \log\pi(a_t\mid s_t) \] and expands the highest-priority partial proof next. This priority is computed from the policy probabilities, not from a separate learned value function. Algorithm~\ref{alg:bestfirst} maintains a frontier of partial proofs, each containing an ordered list of open subgoals and its action history. Here $\Vert$ denotes sequence concatenation. The optional action cap is disabled when $A_{\max}=0$. The pseudocode shows the pop-budget logic; searches also stop at the configured time limit. \begin{algorithm}[tbp] \caption{Policy-guided best-first proof search} \label{alg:bestfirst} \begin{algorithmic}[1] \Require policy $\pi$, initial state $s_0$, pop budget $B$ \Require optional action cap $A_{\max}$ \Ensure a solving action sequence, or \textsc{Unsolved} \State $\textit{frontier} \gets$ max-priority queue keyed by $g$ \State push $(g{=}0,\ \textit{subgoals}{=}[s_0],\ \textit{acts}{=}[\,])$ onto $\textit{frontier}$ \State $\textit{pops} \gets 0$ \While{$\textit{frontier}\neq\emptyset$ \textbf{and} $\textit{pops} < B$} \State $(g,\ \textit{subgoals},\ \textit{acts}) \gets \Call{PopMax}{\textit{frontier}}$ \State $\textit{pops} \gets \textit{pops}+1$ \State $\textit{legal} \gets \Call{LegalActions}{\textit{subgoals}[0]}$ \If{$\textit{legal}=\emptyset$ \textbf{or} ($A_{\max}{>}0$ \textbf{and} $|\textit{legal}|{>}A_{\max}$)} \State \textbf{continue} \EndIf \State $\textit{scores} \gets \pi(\textit{subgoals}[0],\ \textit{legal})$ \State $\log\pi \gets \log\big(\textit{scores}/\!\sum \textit{scores}\big)$ \For{each action $a_i \in \textit{legal}$} \State $\textit{spawned} \gets \Call{Expand}{\textit{subgoals}[0],\ a_i}$ \State $\textit{subgoals}' \gets \textit{spawned}\,\Vert\,\textit{subgoals}[1{:}]$ \If{$\textit{subgoals}'=\emptyset$} \State \Return $\textit{acts}\,\Vert\,[a_i]$ \EndIf \State push $(g+\log\pi_i,\ \textit{subgoals}',\ \textit{acts}\,\Vert\,[a_i])$ onto $\textit{frontier}$ \EndFor \EndWhile \State \Return \textsc{Unsolved} \end{algorithmic} \end{algorithm} \section{Policy Rollout Search} \label{app:rollout-search} Algorithm~\ref{alg:rollout} first runs a greedy trajectory, then up to $n$ sampled trajectories, stopping at the first success. Each attempt starts from a fresh copy of the initial state. The queue contains only the open subgoals of the current trajectory, not alternative partial proofs. Executing an action replaces the focused subgoal with its resulting subgoals; the attempt succeeds when none remain. Here $\pi(a\mid s)$ is the policy distribution over legal actions, and $\Vert$ denotes sequence concatenation. Sampled actions use $\pi_{\tau}(a\mid s)\propto\pi(a\mid s)^{1/\tau}$. The reported evaluations use $n=16$, $D=60$, $\tau=1$, and a single 600-second time budget shared by all attempts. Deadline checks occur between attempts and at the beginning of each action step; an in-progress enumeration, scoring, or execution operation can therefore exceed the time limit. The pseudocode omits exception handling: the implementation abandons an attempt if action enumeration fails, and skips an action whose execution fails, choosing again among the remaining actions at that state. The optional legal-action cap is disabled in these evaluations. \begin{algorithm}[tbp] \caption{Policy rollout search} \label{alg:rollout} \begin{algorithmic}[1] \Require policy $\pi$, initial state $s_0$, sampled attempts $n$, action limit $D$ \Require temperature $\tau$, shared time budget $T$ \Ensure a solving action sequence, or \textsc{Unsolved} \State $\textit{deadline}\gets\Call{Time}{}+T$ \State $\textit{result}\gets\Call{Rollout}{s_0,\textsc{Greedy},D,\tau,\textit{deadline}}$ \If{$\textit{result}$ is solved} \State \Return $\textit{result}$ \EndIf \For{$j=1,\ldots,n$} \If{$\Call{Time}{}>\textit{deadline}$} \State \textbf{break} \EndIf \State $\textit{result}\gets\Call{Rollout}{s_0,\textsc{Sample},D,\tau,\textit{deadline}}$ \If{$\textit{result}$ is solved} \State \Return $\textit{result}$ \EndIf \EndFor \State \Return \textsc{Unsolved} \Statex \Function{Rollout}{$s_0,\textit{mode},D,\tau,\textit{deadline}$} \State $\textit{queue}\gets[\Call{Clone}{s_0}]$; $\textit{acts}\gets[\,]$ \For{$\textit{step}=1,\ldots,D$} \If{$\Call{Time}{}>\textit{deadline}$} \State \Return \textsc{Timeout} \EndIf \If{$\textit{queue}=\emptyset$} \State \Return $(\textsc{Solved},\textit{acts})$ \EndIf \State $s\gets\textit{queue}[0]$; $\textit{legal}\gets\Call{LegalActions}{s}$ \If{$\textit{legal}=\emptyset$} \State \Return \textsc{Dead} \EndIf \If{$\textit{mode}=\textsc{Greedy}$} \State $a\gets\arg\max_{a'\in\textit{legal}}\pi(a'\mid s)$ \Else \State sample $a\sim\pi_{\tau}(\cdot\mid s)$ over $\textit{legal}$ \EndIf \State $\textit{spawned}\gets\Call{Expand}{s,a}$ \State $\textit{queue}\gets\textit{spawned}\,\Vert\,\textit{queue}[1{:}]$ \State $\textit{acts}\gets\textit{acts}\,\Vert\,[a]$ \EndFor \If{$\textit{queue}=\emptyset$} \State \Return $(\textsc{Solved},\textit{acts})$ \EndIf \State \Return \textsc{MaxDepth} \EndFunction \end{algorithmic} \end{algorithm} \section{Conjecture Selection Details} \label{app:selection-details} \paragraph{Statement representation and scores.} The selection tokenizer separates each parenthesis and square bracket from the surrounding text, then splits on whitespace. Variable names, operators, type names, and delimiters therefore contribute to both the token distance and the statement length. These tokens are distinct from the raw character IDs used by the prover's language model. Distances are computed with unit-cost Levenshtein distance. Hardness values are saved best-first queue-removal counts from the starting-prover collection; unsolved candidates are simply not selected. The HN implementation and stores the log-hardness values and pairwise ratios. Hard/length instead uses the raw count $b(c)$ divided by token length. \paragraph{Promotion procedure.} Algorithm~\ref{alg:hn-selection} summarizes the HN selection procedure using the score defined in Equation~\ref{eq:hn-score}. \begin{algorithm}[tbp] \caption{Hard Neighbours selection on a fixed proved pool} \label{alg:hn-selection} \begin{algorithmic}[1] \Require proved candidates $\mathcal{C}$, proved seed references $R_1$ \Require search costs $b$, token distance $d$, batch cap $m$, round cap $T$ \Ensure promoted candidate set $\mathcal{P}$ \State $\mathcal{U}\gets\mathcal{C}\setminus R_1$; $\mathcal{P}\gets\emptyset$; $R\gets R_1$ \For{$t=1,\ldots,T$} \State $\mathcal{E}\gets\{c\in\mathcal{U}:\exists r\in R,\ b(r) A: ???