marozolsCliffordProject

Lean formalization of the structure theorem for the single-qudit Clifford group

Clifford Project

This is an ongoing Lean formalization of the structure theorem for the single-qudit Clifford group, restricted to the case where the dimension is an odd prime. This formalization is based on Sections 2 and 3 of

D. M. Appleby, SIC-POVMs and the Extended Clifford Group, arXiv:quant-ph/0412001, J. Math. Phys. 46, 052107 (2005)

See the HTML blueprint to inspect the current state of the project.

Contributing

This project is part of the Lean seminar at CWI and the University of Amsterdam, coordinated by Maris Ozols and Carli Bruinsma. All participants of the Lean seminar are welcome to contribute. Here is how to get started:

  • Get push access: Share your GitHub username on our Zulip channel so you can be added as a collaborator and push to the repository.

  • First contribution: Clone the repository and add your name to CliffordProject/Authors.lean.

  • What to work on? Browse the HTML blueprint, its summary or dependency graph to find where to contribute.

  • Coordination: Use our private Zulip channel to coordinate efforts and ask questions if you run into any problems.

  • Claim ownership: Before you start working on an item, mark it as yours by adding the (owner := "Your_Name") tag to it in the blueprint. This prevents duplicate effort.

  • Natural language first: Every item should have both a natural language statement and a Lean formalization. If you are formalizing a proof — even a very simple one — first make sure a natural language version exists, is complete, and easy to follow. Most simple lemmas in the blueprint do not yet have natural language proofs, so you will likely need to write one before you start formalizing it.

  • Change everything! You are encouraged to modify everything — definitions, lemmas, and even the main theorems — both their natural language statements as well as Lean formalizations.

  • Adding new items: Feel free to add new items as needed. While the overall proof has been pre-digested, adding well-chosen auxiliary lemmas can make formalization significantly easier. In particular, feel free to break down larger items (especially theorems) into sequences of smaller intermediate lemmas.

  • Keeping things building: It is fine to leave sorrys in your contribution, but please make sure your code type-checks since every commit triggers a GitHub Action that regenerates the HTML blueprint. It is advisable to first build the HTML locally to make sure your contribution does not break anything.

  • AI use: This project could easily be auto-formalized with AI, but that is not our intention — the goal is to learn Lean. Please do the formalization by hand, using AI only for assistance if you get stuck.

Overview

The formalization is organized into the following chapters (in CliffordProject/Chapters/):

ChapterFileSummary
Roots of unityRootsOfUnity.leanDefines the primitive -th roots of unity and , and establishes basic facts about them.
Symplectic formSymplecticForm.leanIntroduces the symplectic inner product on and proves basic properties.
Pauli matricesPauli.leanDefines the generalized single-qudit Pauli operators and acting on and derives their fundamental relations.
Displacement operatorsDisplacement.leanBuilds the displacement operators from the Pauli matrices. They constitute the Pauli/Weyl–Heisenberg group.
Clifford groupClifford.leanDefines the Clifford group as the normalizer of the Pauli group.
Symplectic actionSymplecticAction.leanShows that conjugation by a Clifford element induces an action on displacement operators via a matrix in .
Weyl representationWeylRepresentation.leanConstructs the Weyl (metaplectic) representation, a group homomorphism whose image is the Clifford group.
Clifford group structureCliffordGroupStructure.leanProves that the Clifford group is isomorphic to the semidirect product .

Verso Blueprint

This project uses Verso Blueprint, a Lean package for blueprints that is built upon Verso, which allows one to interleave informal mathematical exposition with formal Lean proofs. The top-level document is CliffordProject/Blueprint.lean.

Building the HTML site

Build and render the blueprint with:

./scripts/ci-pages.sh

This is equivalent to:

lake build CliffordProject
lake env lean --run CliffordProjectMain.lean --output _out/site

Viewing it locally

The generated HTML is written to _out/site/html-multi/. Because the site uses absolute paths, it must be served via a local HTTP server rather than opened as plain files. Use Python's built-in server:

cd _out/site/html-multi
python3 -m http.server

Then open http://127.0.0.1:8000/ in your browser.

Dependencies