Contribute to QuantumComputinglib

Bring one sourced statement to one checked Lean declaration

Submit teaching corrections, external-library mappings, or new state-preparation and block-encoding lemmas. Large changes begin with a proposal so assumptions and module ownership are agreed before proof work.

Draft in the live workspace Open a lemma proposal Prepare a pull request →

Before writing Lean

A small correction or isolated lemma can go directly to a pull request. Start with a proposal when the work adds a module, dependency, public API, mathematical contract, or substantial construction route.

Fix the scope

Record the source, exact statement, conventions, owning module, and whether the wider route is complete.

Reuse before adding

Search the declaration catalog and external atlas. Prefer a narrow adapter to a duplicate API.

Choose the evidence class

Separate a Lean certificate, finite executable check, imported contract, and exploratory argument.

Four steps from idea to an indexed contribution

1
Scope
Agree on the mathematical boundary, source, conventions, owner module, and public API.
2
Develop
Add the smallest focused declaration. Do not use sorry, admit, a new axiom, or a weakened placeholder proposition.

Verify

lake build
lake build ABEISTests
python3 tools/qbe.py check
bash scripts/build-all.sh

Report a gate you could not run; do not mark it passed.

4
Submit and receive credit
Open a focused PR with source, API choices, local and route status, exact gate results, and preferred public credit.

Read the repository-wide contribution policy and integrated contributor record.

Workspace packet and pull request serve different stages

The workspace exports a versioned JSON packet for discussion and review. A pull request carries the implementation. Neither marks itself integrated: maintainers check mathematical equivalence, assumptions, API fit, provenance, license, and the complete ASPBE gate.

Machine-readable packet schema · Open a proposal · Open a pull request

Status words are not interchangeable

Proposed statement or code awaits review.

Lean checked the submitted snippet compiled locally.

Integrated the declaration passed the repository gate and entered the generated inventory.