Who could use Lean for Bio, and what it cannot do for them
Four enumerations, served as versioned JSON and checked by tests: the people and agents with a reason to open this system, the concrete jobs they would bring, the grand questions of biology split into the part a proof can settle and the part only measurement can, and every tool that is missing, ranked by how much it unblocks.
The line this whole page depends on
Every claim below about what Lean settles is a claim about premises, never about organisms. A grand question has a formalisable core exactly to the extent that part of the disagreement about it is a disagreement about what follows from what.
Personas
One entry per person or agent with a reason to use a formalised law registry over biology: what they do today without it, what they would ask, and the tools they need. EXISTS and PARTIAL names were checked against sim-engine/contract.json and mcp/server.mjs, so a name here cannot be invented. MISSING names are proposals defined in the gap list. No persona has an empty tool list; a test enforces that.
Use cases
One row per job, with the tool sequence that answers it today. Answerable today is derived from the step statuses, not asserted: no means a missing step the route cannot be walked without.
Grand questions
The big open questions, each split honestly into (a) the formalisable core, written as conditionals so the premises are visible, and (b) the empirical remainder, item by item, with why no proof reaches it. Then what already exists here towards it, and what a user would still need. Every citation was fetched from Europe PMC or Crossref; both sides are named where the literature disagrees.
Tool gap analysis
The union of every missing tool above, deduplicated. The rank is counted at build time from the personas, use cases and grand questions, so a gap cannot promote itself: one point per distinct persona, use case and grand question that names it, plus one more for each use case that cannot be answered at all without it.
Ranked by how much each unblocks
The same numbers as a table
| # | gap | kind | effort | personas | use cases | questions | score |
|---|
What each kind means
| kind | n | what it means |
|---|---|---|
| tool | A surface over data we can already reach. Buildable now. | |
| lean-module | A Lean file that has to be written and proposed before any tool can serve it. | |
| data | A measurement set we do not have. No tooling creates it. | |
| integration | Wiring to a system outside this repo. |
Effort estimates are judgements written by this thread and have not been validated against any delivery. Nothing here is costed, scheduled or assigned.
Deliberately absent
Things a reader will look for in the gap list and not find, because leaving them out was a decision. Without this section a missing feature is indistinguishable from an oversight.
Get it
MCP
Four read-only tools, no network call, each returning the provenance envelope {result, provenance, scope}.
leanbio_personas { id, text, needs_tool, status, brief }
leanbio_use_cases { id, persona, answerable, tool, uses_gap,
uncomfortable, worked_only, text, limit }
leanbio_grand_questions { id, disputed, has_repo_asset,
core_strength, section, with_citations }
leanbio_tool_gap { id, kind, effort, buildable_now,
unblocks_persona, unblocks_question, limit }
Handlers: pipeline/leanbio/capability-map/tools.mjs. They reach the hosted server once the hub applies sim-engine/tools/CAPABILITY-REGISTER.md and mcp/CAPABILITY-PATCH.md; this page and the static mirror do not wait for that.
CLI
node pipeline/leanbio/capability-map/cli.mjs overview --table node ... cli.mjs personas --needs-tool premise_check --table node ... cli.mjs use-cases --answerable no --table node ... cli.mjs grand-questions --id gq-hamiltons-rule --table node ... cli.mjs tool-gap --kind lean-module --table node ... cli.mjs line
Static API
GET /api/lean/capability/index.json GET /api/lean/capability/personas.json GET /api/lean/capability/use-cases.json GET /api/lean/capability/grand-questions.json GET /api/lean/capability/grand-questions/<id>.json GET /api/lean/capability/tool-gap.json GET /api/lean/capability/citations.json GET /api/lean/capability/schema.json
Built by dashboard/build-lean-api.mjs from the same files, so the mirror cannot drift from the tools.