This example shows TorchLean as a checker around a 3D-vision pipeline. The model and Python exporter are not trusted. They produce a JSON artifact containing a camera matrix, eight 3D box corners, image dimensions, and a claimed 2D box. Lean reloads that artifact, recomputes the projection, and checks the geometry claim.

What This Checks

The checked claim is narrow enough to audit:

camera_P : 3 x 4 projection matrix
corners3d : 8 x 3 cuboid corners
bbox2d : [xmin, ymin, xmax, ymax]

For each corner (x, y, z), the checker forms the homogeneous point [x, y, z, 1], multiplies by the 3 x 4 camera matrix, divides image coordinates by projected depth, and compares the resulting pixel (u, v) with both the image bounds and the claimed 2D box. The depth check matters: a point behind the camera should not be accepted just because its divided coordinates look plausible.

Lean verifies that image dimensions are positive, the box is ordered and inside the image, all eight corners have positive projected depth, every projected corner is inside the image, and every projected corner is enclosed by the claimed 2D box.

The core artifact type is a tensor-shaped camera certificate:

structure BoxCameraCert (α : Type) where
  width : α
  height : α
  tol : α
  camera : CameraP α
  corners : BoxCorners α
  bbox : Box2D α

The executable checker is a Boolean function:

def checkCert (cert : BoxCameraCert α) : Bool :=
  checkPositiveImageSize cert &&
    checkBBoxOrdered cert &&
    checkBBoxInsideImage cert &&
    checkPositiveDepths cert &&
    checkProjectedInImage cert &&
    checkBBoxEnclosesProjection cert

And the theorem connects the executable checker to the theorem-facing contract. The page omits the standard arithmetic/typeclass parameters; the full theorem is in the 3D box verification API:

theorem checkCert_sound
    {cert : BoxCameraCert α} (h : checkCert cert = true) :
    Verified3DBox cert

This is the key pattern: the external model and Python exporter produce data; the Lean checker recomputes the geometric claim from that data.

Run The Real Model Path

The direct 3D detector route uses WildDet3D from Hugging Face. It is optional and heavier than the rest of the site examples, so run it only in an environment where installing model dependencies is okay.

python3 -m pip install -r scripts/verification/geometry3d/requirements-wilddet3d.txt
python3 -m pip install --no-deps utils3d
python3 scripts/verification/regenerate_assets.py --group geometry3d-wilddet3d --run

The command exports and checks:

lake exe verify -- camera-box3d-cert \
  _external/geometry3d/wilddet3d/wilddet3d_cat_box3d_cert.json

It also renders PNG overlays under:

_external/geometry3d/wilddet3d/

The accepted overlay uses the projected 3D footprint as the claimed box. The strict diagnostic overlay uses WildDet3D’s own 2D detection box. On the default demo image, Lean rejects the strict claim because projected 3D corners fall outside that box.

What A JSON Artifact Looks Like

The concrete JSON is deliberately plain so it is easy to produce from any detector, not just WildDet3D.

{
  "format": "torchlean.camera.box3d.v1",
  "width": 640.0,
  "height": 480.0,
  "tol": 1.0,
  "camera_P": [1.0, 0.0, 320.0, 0.0, 0.0, 1.0, 240.0, 0.0, 0.0, 0.0, 1.0, 0.0],
  "corners3d": [0.0, 0.0, 8.0, 1.0, 0.0, 8.0, 1.0, 1.0, 8.0, 0.0, 1.0, 8.0,
                0.0, 0.0, 10.0, 1.0, 0.0, 10.0, 1.0, 1.0, 10.0, 0.0, 1.0, 10.0],
  "bbox2d": [319.0, 239.0, 321.0, 241.0]
}

For Cube R-CNN, Omni3D, or another detector, the workflow is the same: export K or P, image size, corners, and a claimed box, then run the Lean checker.

python3 scripts/verification/geometry3d/export_omni3d_box3d_cert.py \
  --prediction-json output/evaluation/predictions.json \
  --out _external/geometry3d/omni3d_box3d_cert.json \
  --verify

Negative Cases

The demo also includes bad certificates motivated by real glue failures: swapped box layouts, negative depth, wrong projection matrix layout, and 2D boxes that do not enclose projected 3D corners.

python3 scripts/verification/regenerate_assets.py --group geometry3d-visual --run

Green overlays correspond to certificates accepted by Lean. Red overlays correspond to rejected certificates. The point is to check the exported camera and box tensors directly, rather than relying only on the visualization.

The Bug Zoo wrapper re-exports the theorem under a tutorial-facing name:

theorem accepted_camera_box_certificate_is_verified
    {cert : BoxCameraCert α}
    (h : checkCert cert = true) :
    Verified3DBox cert :=
  checkCert_sound h

There is also an interval robustness theorem for perspective division. If homogeneous projection numerator/depth intervals divide into a pixel interval contained in the bbox, every concrete camera choice represented by those intervals stays inside the same bbox. Again, this is the readable shape of the statement; the full theorem includes the interval hypotheses.

theorem homogeneous_projection_uncertainty_stays_inside_bbox :
    xmin cert ≤ uNum / z ∧
      uNum / z ≤ xmax cert ∧
      ymin cert ≤ vNum / z ∧
      vNum / z ≤ ymax cert

Next, read the Bug Zoo walkthrough for the surrounding failure-mode catalog, or the Verification Bounds walkthrough for IBP and CROWN-style graph verification.