Skip to content

README.md

Latest commit

 

History

History
34 lines (20 loc) · 642 Bytes

README.md

File metadata and controls

34 lines (20 loc) · 642 Bytes
Raw

Collatz Lean4 Formalization

Lean 4 formalization workspace for the Collatz SEDT proof chain.

Proof Chain Scope

The project tracks and validates the chain:

D.1 -> {E.2, F.6/F.7, G.5} -> H.main -> I.1

Production Entry

  • Collatz.lean
  • Collatz/Production.lean

Verified Gate Policy

CI enforces proof-chain hygiene for core theorem modules:

  • no sorry
  • no axiom

Gate is configured in .github/workflows/lean.yml.

Build

lake build Collatz

Mapping Sources

  • Lean mapping: Collatz/Documentation/PaperCodeMapping.lean
  • Paper index: ../collatz-paper/paper/src/md/appendices/internal/INDEX.md