Research program
Formal mathematics, cryptographic research, and the infrastructure needed to make long-running AI research inspectable.
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.
We want to learn whether formal-research teams can use that workflow on a second project. External product validation remains open.
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.