Description
KeyAI develops a verified mathematical substrate and autonomous proving engine. Its workflow separates model-generated ideas from kernel-checked proofs: candidate results are drafted, verified with a pinned Lean and Mathlib toolchain, and only accepted into the corpus when they contain no unproven steps or added axioms. Its current work covers secp256k1 arithmetic and generic-hardness statements for the elliptic-curve discrete-log problem, while its roadmap expands toward general elliptic-curve arithmetic and BSD-adjacent formalization infrastructure.