Project status

Corpus at this build

Counted from the repository at site build time. Port counts do not imply complete hardware correctness proofs.

Metric	Count
Paired Python / Lean ports	173
Directories without a port	11
Total TritonBench-G directories	184

Inspect the evidence

Use the searchable proof coverage table to inspect each kernel’s theorem, source functions, numeric model, assumptions, and gaps.

The completion audit records the corpus review. Use the proof-gap manifest and documented blockers to inspect the scope of individual results. A paired port is an inventory entry; its theorem statement, assumptions, and registered deviations determine what has been proved.

The website build counts source files. It does not rerun the Lean proof audits or certify a new audit result.

Reproduce the checks

From the repository root:

lake build
scripts/check-artifact.sh
bench/audit_tritonbench_g.sh

The artifact gate checks proof placeholders, allowed axioms, the kernel manifest, and documentation consistency. The bench audit also checks port elaboration, registered proof gaps, Python/Lean translation patterns, and trust reports. See the artifact workflow and bench workflow for recorded CI runs.

Upstream bug reports

Two reports to PyTorch illustrate silent failures in generated kernels:

• Pooling and reduction: incorrect batch stride (#179931). A generated reduction used 3200 as the batch stride instead of the actual 3185, producing shifted reads and potentially out-of-bounds accesses.
• Slice-scatter backward: collapsed gradient dimension (#180164). A zero stride inherited from a broadcast tensor collapsed an iteration dimension; correct forward outputs masked incorrect gradients.

The reports contain reproduction details and the latest resolution.

Scope and next steps

Read the semantic scope for the boundary between mathematical kernel proofs and external hardware checks. Follow the roadmap for current development work.