1\section{Autonomous Mathematical Discovery Framework}2\label{sec:framework}34The methodological object of this paper is a six-stage pipeline (Figure~\ref{fig:pipeline}) run by an autonomous5agent (Claude Code with the Claude Fable~5.1 model) under the written mandate reproduced in6\code{docs/MANDATE.md}. We describe the stages as implemented, the artefacts each produces, and the rules that keep7the pipeline honest. The pipeline is deliberately simple; its value is measured in Section~\ref{sec:results} by what8it rediscovered, what it rejected, and what it did not claim.910\begin{figure}[htbp]11 \centering12 \resizebox{\textwidth}{!}{\input{figures/fig_pipeline}}13 \caption{The six-stage discovery pipeline (illustrative diagram of the implemented workflow; file names refer to14 the repository). Dashed arrows are the two feedback loops: counterexamples send a hypothesis back to symbolic15 analysis, and evaluation sends it back to generation for refinement or rejection.}16 \label{fig:pipeline}17\end{figure}1819\paragraph{Stage 1: literature extraction.} A structured database (\code{literature/db.yaml}) records theorems,20algorithms, assumptions, complexity bounds, experimental records, open problems and negative results, each with a21source key that must exist in the verified BibTeX file. Verification means that the entry was confirmed against22Crossref, IACR ePrint, a DOI, or the official standard; unconfirmed items are listed separately and never cited.2324\paragraph{Stage 2: hypothesis generation.} Each hypothesis is a file with sixteen mandatory fields (statement,25motivation, assumptions, expected contribution, related work, possible counterexamples, verification strategy,26computational budget, status, classification, evidence, verdict, \ldots), validated by \code{registry.py}, which27also emits the discovery log and Table~\ref{tab:hypotheses}. Hypotheses were generated from three sources: the28mandate's research questions, gaps noted in Stage~1, and the outputs of Stage~3's identity search.2930\paragraph{Stage 3: symbolic investigation.} Two tools. SymPy performs exact polynomial reductions modulo the curve31equations (the six checks S1--S6 of \code{symbolic\_checks.py}: group-law closure, $\phi$ is an endomorphism, the32$x$-only differential addition formula, Semaev's $S_3$, ECDSA malleability, Schnorr correctness). The33\emph{identity search} enumerates 58\,064 candidate relations among twelve constants of \secp{}---binary quadratic34forms $u^2+cuv+dv^2$ against targets $\{p,n,2p,3p,4p,\dots\}$, modular quadratics, linear relations in the GLV basis,35and two negative-control spaces (cross-modulus relations between $\beta$ and $\lambda$; small linear relations36involving the generator's coordinates)---and tests each with exact integer arithmetic. It found 22 identities and370 control hits; every identity is explained by $\beta,\lambda$ being cube roots of unity and by38Proposition~\ref{prop:glv}, which the search itself prompted when it reported $t^2+3b_1^2=4p$ (hypotheses~\Hname{H02},39\Hname{H07}).4041\paragraph{Stage 4: experimental evaluation.} Every experiment is a script that takes a seed and an output path and42writes a JSON document with a provenance block (host, CPU, RAM, OS, library versions, command line, timestamp, elapsed43time) through a single helper (\code{wp34.provenance.record}). Expensive computations use a Rust engine for the ECDLP44and native SAT solvers for SHA-256, distributed over the MacLustr cluster (Section~\ref{sec:design}); the laptop runs45reference checks and figures. A result that is not backed by a saved JSON file does not appear in the paper.4647\paragraph{Stage 5: formal verification.} Statements that are decidable at the bit level are proved in Lean~4 with48\code{bv\_decide}, which compiles a bit-vector goal to SAT, calls CaDiCaL and checks the returned LRAT proof inside the49kernel. Statements about abstract groups are proved against an explicit axiomatisation. Section~\ref{sec:formal}50lists exactly what is machine-checked; everything else in the paper is an informal proof or a measurement, and51conjectures are labelled as such.5253\paragraph{Stage 6: scientific evaluation.} Each hypothesis receives one of six labels---new verified result, known54result independently reproduced, conditional result, empirical observation, rejected conjecture, unresolved55direction---after a literature comparison. The rubric is applied conservatively: a result is ``new'' only if we found no56prior statement of it and it is proved; a reproduction with sharper constants is still ``known''. The complete log is57\code{research\_log/discovery\_log.jsonl}.5859\paragraph{Integrity rules.} Synthetic instances only; no real keys, addresses or blockchain data; no claim that a60computation ran unless its output is saved; operation counts next to wall-clock; at least one negative control per61experimental family; two independent implementations for every arithmetic component. Two development bugs caught62by the last rule (a kangaroo reference whose retry ignored the seed, and a PARI output-parsing error) are logged as63evidence that the rule does work (\Hname{H23}).6465\paragraph{What the framework is not.} It does not search a space of programs or proofs by itself in the sense of66\citet{fawzi2022discovering}, \citet{romeraparedes2024mathematical} or \citet{trinh2024solving}: the hypotheses are67written by the agent, the identity search is a bounded enumeration, and the design-space search of68\Hname{H09} is a parameter sweep. Its contribution is the discipline---structured records, exact checks, provenance,69formal verification, and an honest classifier---applied end to end by one autonomous agent on a problem where the70temptation to over-claim is strong. We assess in Section~\ref{sec:results} whether this discipline produced anything a71careful literature reading would not have.72