Cellcounting

A Lean 4 formalization generated with Tex2Lean. If you are reviewing the formalization, start with Cellcounting/Model/: those files define what the theorems mean. A successful build checks the Lean code, but it cannot tell you whether these definitions and statements match the paper.

What to review

Read Cellcounting/Model/Theorem.lean alongside the paper. Check the theorem's quantifiers, hypotheses, conclusion, and any definitions it uses. In particular, look for assumptions that narrow the claim or change the meaning of an input. Then follow the definitions into the other Model/ files that are present:

• Cellcounting/Model/Prelude.lean defines the shared vocabulary.
• Cellcounting/Model/Prior.lean records assumptions or results taken from earlier work.
• Cellcounting/Model/Operations.lean names project-specific operations and their costs.
• Cellcounting/Model/Program.lean describes the algorithm.
• Cellcounting/Model/Run.lean describes how randomized runs are sampled.
• Cellcounting/Model/Theorem.lean states the project's headline results.

The particular files depend on the project. Compare their definitions with the paper, especially the algorithm, probability distribution, and cost model when those are part of the claim. The proof work is mainly in Cellcounting/Analysis/; Cellcounting/Interface/, when present, connects the model to that proof. Model/Theorem.lean may also contain short proofs that assemble results from Analysis/.

What the generated checks do

The files in Cellcounting/Meta/ contain Lean checks generated by Tex2Lean. They help keep the model reviewable, but they do not decide whether it matches the paper:

• ModelClosure.lean checks that dependencies of theorem statements and program definitions stay in Model/ or in explicitly allowed external modules. Review those exceptions if they matter to the claim.
• CostSeal.lean checks that an algorithm in Model/Program.lean uses the permitted operations and cannot bypass the declared cost accounting. The separate CellcountingTest/CostSealBreaches.lean contains examples that the check is expected to reject.
• Audit.lean imports the project's modules and reports declarations in Model/ that the selected theorem statements do not reach. Such reports are warnings to inspect, not proof that those declarations are wrong.

These files are regenerated as the project develops. Review the checks and any exceptions they allow; change the model or the generator if a check reveals a problem.

Build

lake update
lake exe cache get
lake build

Toolchain: leanprover/lean4:v4.34.1. Configured Mathlib revision: d13f23b723b8a846827a245b89c10fc7d3f11612. Configured arlib revision: d212595017a0bd8688c02a9f4d67a63da5b5ce5c.

After building, inspect any errors or warnings, including declarations that use sorry. For each headline theorem in Cellcounting/Model/Theorem.lean, use #print axioms to check its actual dependencies. A theorem may use none or some of Lean's usual axioms (propext, Classical.choice, Quot.sound); sorryAx or another unexpected axiom needs investigation. These checks establish facts about the Lean development. Reviewing Model/ against the paper is still necessary to judge the formalization itself.