KeyAI is building the verified substrate for a new era of mathematical discovery: an autonomous engine that proposes and proves, on a foundation the Lean kernel certifies line by line — zero unproven steps. It begins at the frontier of elliptic-curve cryptography and reaches toward the deepest open questions in number theory.
KeyAI turns a body of mathematics into a living, verified substrate — re-checkable
from source, pinned to an exact toolchain, navigable by machine. On top of it runs an engine
that proposes, proves, and promotes new results, with the kernel as the gate. Nothing enters the
base unless Lean accepts it with no sorry and no added axioms.
A three-party harness separates ideas from truth: models decompose and draft; a warm Lean toolchain verifies each candidate in seconds; only kernel-accepted results are promoted. The generator only proposes — it never asserts a proof.
Break a target into leaf lemmas; adversarially design proofs.
Tactic ladder + models draft candidate proofs.
The Lean kernel accepts or rejects — no appeal.
Kernel-clean results enter the base via review.
Arithmetic of the secp256k1 curve and generic-hardness statements for the elliptic-curve discrete-log problem: primality of field and group order, torsion structure, the GLV endomorphism, division-polynomial degrees and coprimality, Baby-step/Giant-step and Pollard-ρ bounds, and more.
This is not an attack. Discrete-log hardness (~2128) is unchanged; the value is the verified asset and the reusable engine. Negative and no-go results are first-class. We map the frontier honestly — the kernel forbids wishful thinking.
Browse the full verification ledger → · Open the environment dashboard →
The proving ground: a self-contained verified corpus and a working autonomous pipeline.
LiveThe same machinery produces reusable, curve-agnostic contributions — e.g. the open Mathlib TODO on elliptic divisibility sequences — that benefit the whole library.
In progressThe north star: formalize the machinery around elliptic curves over ℚ — heights, ranks, L-functions — the substrate a future reasoner needs to attack the deepest open problems.
HorizonCorrectness is decided by Lean, not by a model's confidence.
What's verified, assumed, and open — counts that don't drift.
Mathlib pinned; every result re-checks from source.
Ontology + target layers are replaceable across domains.