Discovering and defining new mathematics — under mechanical verification.
We define new mathematical architectures, the methodologies that drive them, and the software tools that make both repeatable. The first target is the Birch & Swinnerton-Dyer conjecture — unconditional, at all ranks, reached through an explicit architecture rather than a single argument, with a buildable Lean substrate underneath.
Four papers open-access on Zenodo · a buildable Lean substrate, zero sorry · two independent routes
Program status
Birch & Swinnerton-DyerThese metrics track how defined and mechanically verified the architecture is — not a claim that BSD is proved.
Architectures, methodologies, and the tools to run them
We define new mathematical architectures, the methodologies that put them to work, and the software tools that make both repeatable. Not to replace mathematical insight, but to help discover and define new results — and to leave a record that can be audited and machine-checked rather than merely believed.
Discovery, not only checking
This is not only a way to check finished proofs. The work is used to discover and define new mathematics, and then to hold what it produces to mechanical verification. The BSD papers and the Lean substrate are the published output of that effort.
AI is the helper — not the author
The mathematical architecture, the decomposition into named hypotheses, and the research methodology are the author’s own work. AI assists in discovering and defining new results — exploration, drafting, and mechanical checking — but it does not author the mathematics. Humans direct; machines verify.
Committed, not merely demonstrated
The BSD program is a committed effort — four archived papers, a 27-module Lean substrate with zero sorry, named conditions, and two routes. We are committed to closing it, and we invite the community to help validate it.
Our goal
Our goal is to define new mathematical architectures, the methodologies that put them to work, and the software tools that make both repeatable — so that progress on a hard problem leaves behind something more durable than a single proof.
The approach →Our first target — BSD
The first target is the Birch & Swinnerton-Dyer conjecture — unconditional, at all ranks, reached through an explicit mathematical architecture rather than a single argument.
We chose BSD as the pilot precisely because it is widely regarded as one of the hardest open problems in mathematics. A methodology that can be made to carry here has earned the right to be pointed elsewhere; one that cannot has told us something useful early, and cheaply.
On status, plainly: the architecture is defined and the route mapped across all ranks. What remains is a finite list of named conditions still to be discharged. Unconditional at all ranks is the target we are working to — not a result we are claiming.
See the BSD case study →From architecture to engine
The longer-term aim is a comprehensive mathematical knowledge engine — and then science-specific engines on the same foundation, each pointed at a different field of research and development.
The emphasis throughout is on deriving new knowledge, not indexing what is already known. BSD is the first problem built this way, and the published record — four papers and a Lean substrate that builds clean — is where to judge whether the approach is working.
See the BSD case study