Live formalization workspace

Read the formula, inspect the Lean statement, then compile

Load a reviewed QuantumComputinglib mapping or edit your own snippet. Formula rendering and declaration navigation work on the static site. Real compilation is available only through the loopback companion server.

Checking the local Lean service

The teaching workspace remains available without code execution.

Execution boundary. GitHub Pages never runs submitted code. ide_server.py binds only to loopback, compiles temporary files under the pinned ASPBE toolchain, and never edits project source.

Mathematical statement

Reviewed mapping

LaTeX

Rendered statement

Lean source

Editable snippet

Declaration page · Source

Lean diagnostics

Local compiler not contacted.

Dependencies

Request review without overstating the result

Name Preferred credit Source or citation

Only the exact Lean text most recently accepted by the local compiler is labeled Lean checked. Editing it invalidates that status.