Formal verification (Lean 4, SAT certificates)

Beyond the Square-Root Barrier: Automated Discovery of Algebraic and Algorithmic Shortcuts in Bitcoin Cryptography

A hypothesis-driven, reproducible study of secp256k1, ECDSA, BIP340 Schnorr and SHA-256 with machine-checked identities and controlled negative results

Simon-Pierre Boucher · UQO Working Papers · November 2026 · v1.0

Bitcoin's security rests on the elliptic-curve discrete-logarithm problem on secp256k1, on SHA-256, and on the ECDSA and BIP340 Schnorr signature schemes. The generic cost of the discrete logarithm, Θ(√n), is a theorem in the generic-group model; the curve's unusual structure, a special prime, j-invariant 0 and…

Zero-Forcing Bounds for Generalized Petersen Graphs: Computational Discovery and Certified Proofs for P(n,5)

Simon-Pierre Boucher · UQO Working Papers · October 2026 · v1.0

The zero forcing number Z(G) of a graph is the minimum size of a set of initially black vertices from which the colour-change rule (a black vertex with exactly one white neighbour forces that neighbour black) eventually colours the whole graph; it bounds the maximum nullity of the matrices described by G. For the…

Beyond One-Step Distributed Maximum Likelihood: Local Bias Cancellation, Global Synchronization, and the Price of Inexact Curvature

A joint order–round frontier, its sharpness in an exact model, and measured communication costs

Simon-Pierre Boucher · UQO Working Papers · October 2026 · v1.0

Distributed maximum likelihood estimation trades statistical efficiency for communication. The paper studies a two-phase protocol in which each of K workers corrects the bias of its local maximum likelihood estimator by an r-th order split-sample extrapolation over nested sub-blocks, the coordinator averages the…