AI Scientist — research loop and next-action reasoning.

Citation-grounded literature reasoning, not plausible paragraphs.

Four interchangeable LiteratureCopilot adapters: a deterministic local fixture for tests, plus PubMed E-utilities, Semantic Scholar Graph API, and Europe PMC REST. Every EvidenceCard carries provenance back to the originating LiteratureQuery; ClaimExtractor pulls typed (subject, predicate, object) triples out of titles and abstracts using the same predicate vocabulary the biology_v* TensorLang modules use, so claims project directly onto a BiologySpec without translation.

peptiter-research-copilot --disease "ulcerative colitis" --max 3
  rank 1: TNF      (score 1.575)
  rank 2: IL23R    (score 1.360)
  rank 3: IL17A    (score 0.525)

Cards collapse into a typed graph; the graph collapses into a verifiable mechanism.

EvidenceGraph normalizes BiologicalEntities across cards (ontology+ID when present, canonical label otherwise) so PubMed and Europe PMC mentions of the same target collapse to one node. Edges aggregate confidence and uncertainty across supporting triples and carry counterevidence references. EvidenceGraphMechanismBridge converts the typed graph + framing into a PathwayMechanismHypothesis the existing PathwayMechanismVerifier accepts — closing the loop from research evidence to the Lean-verifiable mechanism path.

JSON-RPC tools, untrusted by default, every invocation logged.

MCPProtocol gives JSON-RPC 2.0 envelopes, typed Tool / Resource / Prompt schemas, and an MCPDispatcher that routes calls to a server. LiteratureMCPServer exposes the four LiteratureCopilot adapters as MCP tools (literature/search, literature/list_adapters) plus a notebook resource. LeanVerifierMCPServer wraps the existing LeanExternalVerifier so external agents can drive the biology_v1/v2 contract through MCP without bypassing the typed hash-bound receipt.

mcp.dispatch tools/call name=literature/search
  arguments: { queryID, adapter: "fixture", disease: "ulcerative colitis" }
  → cards: [...], rankedHypotheses: [...], notebookEntry: {...}

Per-path attribution + signed-mechanism theorems alongside hash binding.

Phase 4 closes the gap between the TensFormer spine and the AI Scientist surfaces above. emit_biology_v2.py enumerates 23 signed paths through biology_v2; BiologyV2.lean's 14 signed-sum + 28 path-count theorems all native_decide and lake build is green. The Swift LeanExternalVerifier.Receipt now carries the attribution report so reviewers see both protective and risk paths per peptide × endpoint, not just the summed sign.

Approval gates encoded as code, not policy memos.

AssayPlan captures objective, materials, candidates, controls, dose schedule, plate map, accept/reject criteria, risk class, approval status — all Codable. AssayPlanDrafter takes a verified mechanism and emits a draft plan whose approval state is .readyForReview only when every gate passes: vehicle present, dose schedule spans 3 orders of magnitude, plate map has no double-assigned wells, risk screen returns no biosecurity or dual-use flags. Otherwise the plan lands in .rejected with the specific reason — a reviewer never sees an unsafe plan in the queue.

Belief state flips on every assay outcome.

LabJob has a one-way state machine (drafted → approved → queued → running → returned → analyzed); out-of-order transitions throw rather than silently advancing. LabJobQueue persists Codably. CandidateBelief is a Beta(α, β) conjugate prior whose ingest() flips next-experiment selection on every outcome — positive bumps α, negative bumps β, inconclusive widens without bias; pickNextExperiment chooses the highest-posterior-variance candidate.