\section{Autonomous Mathematical Discovery Framework}
\label{sec:framework}

The methodological object of this paper is a six-stage pipeline (Figure~\ref{fig:pipeline}) run by an autonomous
agent (Claude Code with the Claude Fable~5.1 model) under the written mandate reproduced in
\code{docs/MANDATE.md}. We describe the stages as implemented, the artefacts each produces, and the rules that keep
the pipeline honest. The pipeline is deliberately simple; its value is measured in Section~\ref{sec:results} by what
it rediscovered, what it rejected, and what it did not claim.

\begin{figure}[htbp]
  \centering
  \resizebox{\textwidth}{!}{\input{figures/fig_pipeline}}
  \caption{The six-stage discovery pipeline (illustrative diagram of the implemented workflow; file names refer to
  the repository). Dashed arrows are the two feedback loops: counterexamples send a hypothesis back to symbolic
  analysis, and evaluation sends it back to generation for refinement or rejection.}
  \label{fig:pipeline}
\end{figure}

\paragraph{Stage 1: literature extraction.} A structured database (\code{literature/db.yaml}) records theorems,
algorithms, assumptions, complexity bounds, experimental records, open problems and negative results, each with a
source key that must exist in the verified BibTeX file. Verification means that the entry was confirmed against
Crossref, IACR ePrint, a DOI, or the official standard; unconfirmed items are listed separately and never cited.

\paragraph{Stage 2: hypothesis generation.} Each hypothesis is a file with sixteen mandatory fields (statement,
motivation, assumptions, expected contribution, related work, possible counterexamples, verification strategy,
computational budget, status, classification, evidence, verdict, \ldots), validated by \code{registry.py}, which
also emits the discovery log and Table~\ref{tab:hypotheses}. Hypotheses were generated from three sources: the
mandate's research questions, gaps noted in Stage~1, and the outputs of Stage~3's identity search.

\paragraph{Stage 3: symbolic investigation.} Two tools. SymPy performs exact polynomial reductions modulo the curve
equations (the six checks S1--S6 of \code{symbolic\_checks.py}: group-law closure, $\phi$ is an endomorphism, the
$x$-only differential addition formula, Semaev's $S_3$, ECDSA malleability, Schnorr correctness). The
\emph{identity search} enumerates 58\,064 candidate relations among twelve constants of \secp{}---binary quadratic
forms $u^2+cuv+dv^2$ against targets $\{p,n,2p,3p,4p,\dots\}$, modular quadratics, linear relations in the GLV basis,
and two negative-control spaces (cross-modulus relations between $\beta$ and $\lambda$; small linear relations
involving the generator's coordinates)---and tests each with exact integer arithmetic. It found 22 identities and
0 control hits; every identity is explained by $\beta,\lambda$ being cube roots of unity and by
Proposition~\ref{prop:glv}, which the search itself prompted when it reported $t^2+3b_1^2=4p$ (hypotheses~\Hname{H02},
\Hname{H07}).

\paragraph{Stage 4: experimental evaluation.} Every experiment is a script that takes a seed and an output path and
writes a JSON document with a provenance block (host, CPU, RAM, OS, library versions, command line, timestamp, elapsed
time) through a single helper (\code{wp34.provenance.record}). Expensive computations use a Rust engine for the ECDLP
and native SAT solvers for SHA-256, distributed over the MacLustr cluster (Section~\ref{sec:design}); the laptop runs
reference checks and figures. A result that is not backed by a saved JSON file does not appear in the paper.

\paragraph{Stage 5: formal verification.} Statements that are decidable at the bit level are proved in Lean~4 with
\code{bv\_decide}, which compiles a bit-vector goal to SAT, calls CaDiCaL and checks the returned LRAT proof inside the
kernel. Statements about abstract groups are proved against an explicit axiomatisation. Section~\ref{sec:formal}
lists exactly what is machine-checked; everything else in the paper is an informal proof or a measurement, and
conjectures are labelled as such.

\paragraph{Stage 6: scientific evaluation.} Each hypothesis receives one of six labels---new verified result, known
result independently reproduced, conditional result, empirical observation, rejected conjecture, unresolved
direction---after a literature comparison. The rubric is applied conservatively: a result is ``new'' only if we found no
prior statement of it and it is proved; a reproduction with sharper constants is still ``known''. The complete log is
\code{research\_log/discovery\_log.jsonl}.

\paragraph{Integrity rules.} Synthetic instances only; no real keys, addresses or blockchain data; no claim that a
computation ran unless its output is saved; operation counts next to wall-clock; at least one negative control per
experimental family; two independent implementations for every arithmetic component. Two development bugs caught
by the last rule (a kangaroo reference whose retry ignored the seed, and a PARI output-parsing error) are logged as
evidence that the rule does work (\Hname{H23}).

\paragraph{What the framework is not.} It does not search a space of programs or proofs by itself in the sense of
\citet{fawzi2022discovering}, \citet{romeraparedes2024mathematical} or \citet{trinh2024solving}: the hypotheses are
written by the agent, the identity search is a bounded enumeration, and the design-space search of
\Hname{H09} is a parameter sweep. Its contribution is the discipline---structured records, exact checks, provenance,
formal verification, and an honest classifier---applied end to end by one autonomous agent on a problem where the
temptation to over-claim is strong. We assess in Section~\ref{sec:results} whether this discipline produced anything a
careful literature reading would not have.