Abducer

Overview

Abducer is a typed, replayable research system for constructing, comparing, testing, and retaining abductive theories over difficult mathematical and scientific problems. It preserves a problem's conceptual alternatives, evidence, failed attempts, proof obligations, and research history rather than treating discovery as a single answer or confidence score.

The repository has two related execution surfaces: a KB theorem-assistance workflow and the canonical theory-first discovery runtime. The latter uses typed operator requests and receipts, isolated branches, semantic events, and single-writer state commits. Getting started explains which surface to use.

Key concepts

• Persistent epistemic state: retain hypotheses, literature, conceptual systems, transformations, failures, and learned results.
• Plural conceptual exploration: mature structurally different candidates and preserve dissent and partial failure.
• Separate authorities: conceptual preference, executable evidence, proof status, publication, and durable state mutation have different contracts.
• Replayable transitions: bind requests, receipts, outputs, and commits to exact target, run, generation, and digest identities.
• Governed continuation: use obligations, budgets, stopping rules, and reflection to determine what may happen next.

Getting started

Use Python 3.11 or newer and the committed uv.lock environment:

uv sync --locked
uv run python skills/orchestration/kb-orchestrator/scripts/run_orchestrator.py --help
uv run python agentic/scripts/run_canonical_discovery_cycle.py --help

These commands inspect both execution surfaces without launching a research run. The default local path does not require provider credentials. Read the first-use guide before selecting a target: some commands intentionally write canonical target state and are unsuitable as disposable smoke tests.

Examples

For theorem assistance, a problem such as P vs NP is represented in KB/*.kb.md; skills connect statements, form and evaluate hypotheses, and maintain proof obligations. For theory-first discovery, a cycle consumes an exact request and validated operator receipts before reducing semantic events into one state commit.

The detailed project guide preserves the conceptual cycle, named workflow functions, and result locations. The named workflow guide explains activation, composition, stopping rules, and handoffs. Case studies show target-specific applications and their claim boundaries.

Architecture

problem and literature → conceptual branches → critique and typed evidence
                       → semantic reduction → atomic epistemic-state commit
                       → post-commit proof and delayed experiment work

agentic/ contains the typed discovery runtime and state; skills/ holds scientific skills; KB/ grounds targets; InformalMathLib/ retains mathematical memory; phyp/ publishes proof hypotheses; artifacts/ holds target outputs. proj_skills/ and prism_me/ support repository maintenance and request controls.

See the architecture overview, data contracts, and research methods.

Documentation

Start with the documentation index. All project documentation uses the same reading areas; specialist collections retain their stable paths.

• Getting started — Install the environment and complete a first example.
• Concepts — Understand the project model, terminology, and evidence boundaries.
• Guides — Carry out tasks and interpret their outputs.
• Architecture — Understand components, data flow, contracts, and extension points.
• Reference — Look up commands, skills, workflows, and documentation sources.
• Development — Change the project and run the relevant checks.
• Operations — Configure, run, observe, and release maintained workflows.
• Governance — Check licensing, provenance, review, and publication requirements.
• Archive — Find historical material and distinguish plans from current behavior.

Development and validation

Start with AGENTS.md and its Prism ME request controls. Documentation, workflow health, architecture reporting, and framework-paper support remain separate from mathematical reasoning. See development.

uv run pytest -q tests/infrastructure/test_documentation_layout.py

Use testing guidance and the affected runtime's focused contract, adversarial, and integration tests for behavioral changes. Passing tests provide scoped implementation evidence rather than theorem correctness.

Limitations and status

This is a research system under active development. Generated hypotheses, conceptual preference, rendered reports, and workflow completion do not establish mathematical truth. The older deterministic abductive loop still has prompt-driven checkpoints. latest reports are convenience projections; scientific authority remains bound to exact artifacts and state identities. Proof and descendant experiments have their own post-commit authority and eligibility rules.

Dependencies and license

Repository source headers identify first-party code as MIT licensed. See LICENSES, REUSE.toml, DEPENDENCIES.md, and software disclosure for source, dependency, attribution, and disclosure boundaries.