Skip to content

ARTIFACT_CHECKLIST.md

Latest commit

 

History

History
71 lines (46 loc) · 2.25 KB

ARTIFACT_CHECKLIST.md

File metadata and controls

71 lines (46 loc) · 2.25 KB
Raw

Artifact Checklist

All counts below are generated by scripts/metrics.sh and must match the README header table and premise/final.json.

Toolchain

Component Version Pinned?
Lean v4.29.0-rc6 Yes (lean-toolchain)
Mathlib4 fde0cc508f Yes (lakefile.lean + lake-manifest.json)
Lake bundled with Lean Yes

Build

# Prerequisites: elan (https://github.com/leanprover/elan)
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

# Build (first run fetches Mathlib)
lake build

# Subsequent builds with cached Mathlib: ~2 minutes (incremental)

Expected build time (local, clean): 15-25 minutes (dominated by Mathlib compilation).

Expected build time (GitHub Actions, clean): 60-90 minutes (slower runners, Mathlib fetch on cache miss).

Expected build time (cached Mathlib): 1-3 minutes locally, 5-10 minutes on CI.

Expected output: 0 errors.

Sorry Inventory

Zero sorry tactics exist in the kernel. Every compiled theorem is proved.

The universal trichotomy (BHMZ STOC 2021) is commented out as a TODO in Theorem/Extended.lean; it is not compiled and does not appear in the theorem count.

CI enforcement: The GitHub Actions workflow fails if any sorry tactic is found. The check matches only standalone sorry tactics (^\s*sorry\s*$), not comment mentions.

Verification Commands

# Count sorrys (should print 0 lines)
grep -rn --include="*.lean" -E '^[[:space:]]*sorry[[:space:]]*$' FLT_Proofs/
# Expected: no output

# Generate canonical metrics (should match README and premise/final.json)
./scripts/metrics.sh

# Full build from clean state
rm -rf .lake/build
lake build

Default Target

The default Lake target is FLT_Proofs (all 53 files). A second target WorldModel builds the proof operad (8 files). Both permit sorry (Lean's default). The CI workflow enforces the sorry ceiling independently.

File Inventory

All counts generated by scripts/metrics.sh:

  • 53 .lean files in FLT_Proofs/
  • 21,522 lines of Lean4
  • 354 theorem/lemma statements (248 public, 106 private)
  • 257 definitions
  • 59 structures
  • 0 sorry tactics

World model (world_model/WorldModel/): 1,170 lines, 0 sorry, 27/27 tests pass.