BanditRLlib Live Formalization

LaTeX, retrieval, candidate Lean, and the compiler in one workspace.

Study reviewed mappings or enter a new bandit/RL claim. GitHub Pages runs neither arbitrary code nor a model API. In local verified mode, a loopback-only service retrieves compiled BanditRLlib declarations and Mathlib/LML cards; an optional model API behind that local service may generate candidate Lean before the exact candidate is sent to the pinned compiler.

Open the workspace Read the verification workflow

Two honest execution modes

Static BanditRLlib site

LaTeX preview, reviewed math↔Lean mappings, source navigation, retrieval examples, dependency trees, and packet export work in any browser. Arbitrary code and model APIs do not run.

Local verified mode

ide_server.py binds to loopback, keeps API credentials server-side, retrieves the current library, and invokes lake env lean on temporary files without repository writes.

Honest statuses

Candidate Translation, Lean-Compiling, Semantically Reviewed, Proof Verified, and Integrated into BanditRLlib are separate states. A compiling candidate is not automatically a faithful translation.

Security boundary. The compile endpoint is intentionally local-only. Do not forward the IDE server through a public or temporary tunnel; use the existing static sharing server for reviewers.

Live formalization workspace

Mathematical statement

Reviewed mapping

Natural-language statement LaTeX

Live rendering

Choose a declaration to begin.

Lean source

Editable snippet

Open declaration page Open source line

Compiler diagnostics

Local Lean service has not been contacted yet.

Lean dependency tree

Choose a reviewed declaration to draw its teaching dependencies.

Candidate formalization record

translation: candidate · Lean: not checked · proof: unproved · library: proposed

Candidate interpretation

No new candidate requested.

Candidate Lean statement

No new candidate requested.

Assumptions

None returned.

Reused BanditRLlib declarations

Run local formalization to retrieve the current library.

Mathlib candidates

None returned.

LML candidates

None returned.

Unresolved proof obligations

Semantic review and repository integration remain required.

Community handoff. Export produces a local JSON draft; it does not upload code or claim verification. Review the packet, add source and contributor details, then follow the community contribution guide.

A narrow certificate boundary for a researcher IDE

The browser edits and visualizes; the loopback companion alone may retrieve repository evidence, call an optional provider through environment-only credentials, compile temporary Lean, and return diagnostics. The server never writes repository source. The exported packet is the integration seam into the ABRL reviewer pipeline.

flowchart LR
    Input["LaTeX or plain-English target"] --> Retrieve["Grounding retrieval<br/>BanditRLlib + Mathlib + LML"]
    Retrieve --> Provider{"Server-side provider<br/>configured?"}
    Provider -->|no| Draft["Draft scaffold<br/>explicitly not formalized"]
    Provider -->|yes| Candidate["Lean statement candidate<br/>assumptions shown"]
    Candidate --> Compile["Temporary Lean compile<br/>loopback service"]
    Compile --> Result["Diagnostics + unresolved obligations<br/>separate semantic, Lean, proof, library status"]
    Draft --> Result
    Result --> Packet["Exported contribution packet<br/>no repository write"]
    Packet --> Harness["ABRL intake and review"]
    Harness -->|only after full gate| Library["BanditRLlib main"]

BanditRLlib Live Formalization: grounded candidate generation, local compilation, review obligations, and ABRL intake · editable Mermaid source

Next: proof states

Attach a persistent Lean language-server session so cursor position can reveal goals, hypotheses, and tactic state without recompiling a whole snippet.

Available: grounded candidates

The provider-independent adapter retrieves BanditRLlib, Mathlib, and LML evidence before generation. With no provider configured, it clearly reports that formalization is unavailable.

Next: community submission

Let an authenticated compiler validate a lemma packet, open a public proposal or branch, attach diagnostics, and preserve contributor credit through review.