Bitcoin's security rests on the elliptic-curve discrete-logarithm problem on \secp{}, on SHA-256, and on the ECDSA
and BIP340 Schnorr signature schemes. The generic cost of the discrete logarithm, $\Theta(\sqrt n)$, is a theorem in
the generic-group model; the curve's unusual structure---a special prime, $j$-invariant~0 and complex multiplication by
the Eisenstein integers---has long invited speculation that an algebraic shortcut might exist. We test this
speculation with an autonomous, six-stage discovery pipeline (verified literature base, 25 structured hypotheses,
exact symbolic checks, seeded experiments with full provenance, Lean~4 machine-checked statements, six-way
classification) executed by an AI research agent under a written mandate that forbids assuming shortcuts exist.
Results. (i)~Every \secp{} parameter and invariant is verified twice with exact arithmetic; $\End(E)=\Z[\omega]$ leaves
nothing beyond the six automorphisms; the GLV lattice is the ideal $(\bar\pi-1)$, which gives the hard-coded
\libsecp{} constants in closed form ($a_1=(t-f)/2-1$, $b_1=-f$); the automorphism orbits admit no compatible group
law; prime-field index calculus and all transfer attacks are excluded quantitatively. (ii)~A native engine solved
$6\,240$ synthetic ECDLP instances of 20--56 bits: empirical exponents $0.48$--$0.50$, rho constant $1.254\sqrt n$
against the random-mapping prediction $1.2533$, order-6 classes $2.42\times$ fewer iterations ($\sqrt6$) but no
wall-clock gain in our implementation, $22\times$ parallel speed-up on 28 threads, the predicted time--memory and
preprocessing trade-offs ($1.5\sqrt{n/T}$ online), and no iteration-function design below the random-mapping floor.
(iii)~BIP340 batch verification reaches $3.1\times$ and saturates for an identified reason; ECDSA and Schnorr verify
at the same cost and differ in proof structure. (iv)~Reduced-step SHA-256 diffuses fully in six steps, shows no
first-order regularity beyond five, and yields to generic SAT search only up to 18-step collisions and $2^{16}$-bit
preimages, far below the 31-step records; the 9-step local collision is reproduced and its linear part proved.
(v)~Lean~4 proofs of the word-level identities, the bijectivity of the step and of all four $\Sigma/\sigma$
functions (refuting our own conjecture that $\sigma_0,\sigma_1$ are singular), the schedule inversion, the
linearised local collision, ECDSA malleability and Schnorr correctness. The pipeline produced sixteen reproductions
with measured constants, six empirical observations, three rejected conjectures and no claim of a weakness; we argue
that this is the correct output for automated mathematical research on cryptographic standards, and we release
everything needed to reproduce it.