Research archive
Historical work in formal mathematics, cryptographic research, and research infrastructure. KeyAI is inactive; published evidence remains available for review.
01 / Cryptographic research
Our reference problem is recovering the discrete logarithm in the prime-order secp256k1 group. Work includes curve arithmetic, torsion structure, polynomial relations, generic-model bounds, and the applicability of proposed routes.
The public route map retains 17 routes, including their evidence, assumptions, and reasons to stop or reopen them. The current decision records 0 promoted attack routes.
No efficient unknown-target secp256k1 solver or validated subgeneric route is claimed. A scoped algebraic result does not establish a practical attack.
02 / Formal mathematics
The Lean libraries contain elliptic-curve formalizations alongside a separate body of complex analysis and elementary number theory. Source-linked ledger entries disclose declarations and proof trust.
Exploratory Riemann Hypothesis work currently provides definitions, reformulations, and symmetry infrastructure. It claims no proof candidate and no progress on RH itself.
Read the formal results →03 / Research infrastructure
Research OS records how a question becomes a proposal, a checked attempt, a retained outcome, and a next decision. The current repository is its public reference deployment.
External product validation remains open. The initiative is inactive and no external pilot is being recruited.
See how Research OS works →Inspect the work
Formal result · Kernel audited
Over the algebraic closure, secp256k1 has 16 points killed by multiplication by four, forming a group isomorphic to (Z/4Z)².
Formal result · Kernel + compiler
A formal primality certificate establishes that the secp256k1 field modulus p is prime.
Formal result · Kernel standard
An entire complex function bounded by C · (1 + |z|)ⁿ is represented by a polynomial of degree at most n.