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