ABEIS Oracle-to-Block-Encoding Task Builder

Target Oracle

Paste a LaTeX operator, matrix formula, or natural-language oracle requirement. This testing preview creates a task packet for ABEIS agents; Lean is still the final verifier.

Task name Mode Harness strategy

Run location and API ownership

The public page should run with the user's own resources. For a static deployment, this section generates a runner packet; a self-hosted runner can read the same fields and call the user's API.

Run location API provider Default model Runner endpoint User API key Redact API key from generated Markdown

Preferred report language

Operator or oracle description

Normalizer alpha Block projector / clean state

Known baseline construction, if any

User / Pro insight injection

Optional external ideas enter the insight pool. In Game Harness mode, the Game Council decides whether they go to the Natural-Language Team for proof review, to the Lean Team for formalization, or to rejected-route memory. They are never plotted as achieved solutions until Lean certifies them.

User intuition or strategy notes ChatGPT Pro / external AI advice Proposed candidate block encoding Proposed proof or correctness argument Injection policy

Constraints and free parameters

Executable exports after Lean certification

ABEIS treats Lean as the proof authority. These options request runnable artifacts after the matching Lean theorem is accepted.

Qiskit Python circuit and finite assertions QuantumKatas-style task and tests OpenQASM 3 transcript and parser/smoke checks Concrete export instantiation

Agent backend preferences

These preferences are written into the generated ABEIS packet. The website does not call model APIs; your local harness or server runner maps them to installed CLIs or wrappers. In Game Harness mode, the Natural-Language Team and Lean Team each have upper/middle/lower layers. They compete in their own language, then exchange useful insights through the Game Council.

Upper Middle Natural-Language Team lower Lean Team lower/formalizer Optional verifier Reviewer

Generated Agent Packet

ABEIS acceptance and ranking

Correctness is accepted only after Lean proves unitarity and the requested block-entry theorem.
Compare asymptotic tiers first: polylogarithmic growth beats polynomial growth.
Inside one tier, rank by gate count, then depth, then auxiliary qubits, then unresolved oracle calls.
After Lean certification, generate the selected Qiskit, QuantumKatas, or QASM artifacts for users.
When a run closes, compare harnesses by generated exact/approximate evolution curves and circuit storyboards.

Run dashboard contract

Per-harness status: active phase, current champion, blocked leaf, and next action.
Exact and approximate BE curves: only Lean-certified candidates are plotted as achieved points.
Circuit storyboard: one diagram per certified exact/approximate candidate.
Reports: selected-language summary, ChatGPT Pro prompt when unresolved, and user-copyable LaTeX proof after Lean closure.

Run dashboard preview

Local mode: run ABEIS in the downloaded repository and paste `reports/<task-id>/dashboard.json` or `evolution.json` here. Hosted mode: connect this page to a user-owned runner endpoint or API-backed service, then render the same JSON outputs.