MathIdeasResearch in progressRepository ↗
← Research catalogOriginal Markdown ↓
On this page

Research evidence platform: bounded pilot specification

The first pilot solves one task: produce a traceable report showing what a pinned mathematical source actually supports for a proposed software claim. Its value would be fewer unsupported guarantees and less reviewer preparation time. No paid pilot, market demand or independently verified proof backend exists yet.

User flow and deliverable

A reviewer selects a source revision, a theorem statement and a proposed use. The report presents the statement's quantifiers, assumptions, selected formal coverage and operational obligations. Gaps are linked to evidence and grouped by the next action needed: source reading, model correspondence, algorithm construction, numerical validation or buyer validation. A complete documentation manifest remains visibly separate from a verified claim.

The pilot covers one repository revision and ten reviewed claims. Thirteen curated contracts now exist; select ten operational claims for the measured pilot. The tenth covers the graph switch-chain kernel, complete-host assumption and all-step time counter, a distinct failure mode. Include the scalar inverse-boundary/new joint-operator mismatch, QAOA ordered limit, basis-exclusion scope gap, GAD decoding assumption, pure-beta normalization premise and Artin membership complexity omission.

Data records

Record Minimum fields Purpose
Source snapshot repository, commit, path, SHA-256, retrieval time Reproduce the exact material reviewed
Statement stable ID, version, source locations, formula/text, quantifiers, assumptions, claim type Prevent a family-level badge from covering every revision
Scope relation statement ID, formal statement ID, reviewed coverage, exclusions, reviewer and date Record a human comparison without equating it with a proof check
Verification run toolchain, checker/config hashes, imports, command, environment, exit result, trust mode, logs Establish what was actually checked in a trusted environment
Dependency edge source statement, target statement, relation, exact evidence location, status Trace explicitly supported impacts of a correction or withdrawal
Operational claim use, input model, implementation revision, asserted guarantees, obligation references Make the bridge to software reviewable
Numerical or finite run fixture and code hashes, arithmetic model, budget, result, comparison baseline Preserve the practical evidence separately from the theorem
Review decision unknown/supported/contradicted, evidence IDs, rationale, reviewer, date Permit corrections and retain earlier editions

Store the pilot as versioned JSON records and a generated local Markdown report. A SQLite read model can index those records later, once query needs are shown. Keep source records and reviewer decisions immutable by edition; a correction adds a new decision and explicit supersession link. No schema should infer that a cited file is valid evidence merely because it exists.

Existing components and remaining implementation

inventory.py locates all 372 families and 719 manuscripts. proof_preflight.py scans configuration/module presence and external-kernel settings. withdrawal_impact.py extracts three explicit withdrawal notices and two dependency edges. audit_claim_contract.py handles thirteen manually curated source/model contracts and rejects documentary mismatches. None runs a trusted theorem prover or verifies the contents of supplied evidence.

A canonical source-hash manifest and joined report now exist for one illustrative claim. All thirteen contracts now have exact file pointers in the enriched registry; next add precise section/line reading records and retain per-contract selected-scope conclusions. Verification-run ingestion should initially accept only authenticated locally produced runs with explicit trust metadata; a proof backend remains separately queued. Do not label imported or unsigned logs as independently verified.

Pilot validation and earning decision

Select ten public claims before measuring performance, with a mix of known gaps and appropriate narrower claims. Have an expert review the same inputs manually and with the report. Record preparation time, correctly found material gaps, missed gaps, false alarms and correction time. Known-gap fixtures test detection; they do not establish general recall or buyer value. A pilot succeeds technically only if each material issue is traceable and the expert can revise incorrect mappings without losing provenance.

For an illustrative AUD 10,000 integration fee at an assumed AUD 180 per specialist hour, direct labor must stay well below 56 hours and leave room for support, sales and overhead. Reuse of records and adapters must be measured. A low-effort report with no recurring decision value is insufficient for subscription pricing; a useful but highly bespoke review may support consulting instead.

External outreach, pricing validation, paid compute, publication and deployment remain outside this research task. Independent next work includes precise section/line enrichment, reproducibility checks and further manuscript review. An expert comparison remains prepared and unperformed; external outreach requires explicit authorization.

Graph protocol addition

The ten-contract registry and new graph-chain report preserve the added contract and one self-authored known-gap claim. The report flags nine documentary gaps. Its finite host-disconnection fixture is saved separately. The older evidence report retains the nine-contract edition. Ten registry entries do not mean ten operational claims have undergone expert comparison; prepare those inputs and their exact source locations before measuring reviewer benefit.

Computational semantics extension

The thirteen-contract edition adds logspace language equality, uniform finite-metric k-server and continuous Brenier stability. Exact source file locations are included for these three; the older ten now have exact file pointers in the enriched edition; line/section and deeper-reading evidence remains a separate task. Select the ten pilot inputs before measuring performance and include narrower positive controls, rather than counting all thirteen registry entries as completed claim reviews.

The computational-model report flags eleven gaps in a self-authored zero-startup claim. Movement and transport references supply finite controls. 65 source-level definition observations preserve per-name meanings and source hashes. Neither fixture detection nor source-text correspondence is the expert/customer workflow comparison. No supplied evidence or imported proof is automatically authenticated.

Ten concrete review inputs prepared

The preserved packet contains eight intentionally mismatched scenarios and two synthetic narrower documentary controls. All ten use public pinned research, but the proposed software claims and support statuses are self-authored controls, not real customer or published application assertions. Source-only and report-assisted cards, a separate self-authored answer key, blank review result fields and archived tool/input hashes make the next comparison reviewable.

All thirteen contracts now have exact source file pointers. This is metadata enrichment, not a claim of new full-file reading or independent proof verification. 25 finite packet controls establish fixture/code consistency only. Expert preparation time, independently adjudicated precision/recall, correction effort and buyer value remain unmeasured. No outreach was authorized or performed.

Use independent reviewers or counterbalanced assignment to reduce repeat-reading effects. Do not treat a faster second exposure as report benefit. Before claiming an expert result, retain actual reviewer identity, source evidence, timing and independent adjudication. Until then this task remains a prepared local experiment.