KeyAI Research · Independent research
We study elliptic-curve cryptography, formalize mathematics in Lean, and build tools that connect AI research to evidence other people can check.
Each entry has a source and a scope.
How to read the evidence
Selected results
These examples explain what a checked statement gives you, where it stops, and how to inspect it.
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.
Our research
Our cryptographic program studies the discrete-logarithm problem on secp256k1, including algebraic structure, proposed routes, and the evidence needed to evaluate them.
We also develop reusable formal analysis and number theory in a separate ResearchOS ledger.
The repository does not solve ECDLP. No secp256k1 break or proof of the Riemann Hypothesis is claimed.
Explore the research directions →Research OS · In development
A research project needs more than its latest successful proof. It needs the sources, failed attempts, assumptions, and decisions that explain what to do next.
Research OS connects those records in a public reference deployment. A hosted multi-project product is not yet available.
For researchers and technical collaborators
We welcome proof review, reproducibility work, and conversations with teams building AI for mathematics. We are also recruiting a formal-research team to test the Research OS workflow.
Find a way to collaborate