Lamport Proof v0.2.0

Lamport Proof v0.2.0

Make an existing proof easier to inspect by exposing its hierarchy, dependencies, scope, and unresolved obligations. Version 0.2.0 organizes that work into three complementary Codex skills:

• $convert-lamport renders a prose proof as a source-mapped hierarchy without repairing it.
• $forward-lamport checks the hierarchy from assumptions to conclusion.
• $reverse-lamport traces the stated conclusion back through the proof-supplied route.

This release also adds a deterministic behavioral evaluation corpus, isolated local skill staging, and contributor, citation, security, and CI material for public development.

Breaking change

$audit-lamport-proof has been renamed to $forward-lamport, with no compatibility alias. $reverse-lamport keeps its existing identifier. Disable or remove a lamport-proof-toolkit v0.1.0 installation before enabling v0.2.0, because the old and new versions both expose $reverse-lamport.

Install

python3 "${CODEX_HOME:-$HOME/.codex}/skills/.system/skill-installer/scripts/install-skill-from-github.py" \
  --repo WWresearch/lamport-proof \
  --ref v0.2.0 \
  --path skills/convert-lamport skills/forward-lamport skills/reverse-lamport

Restart Codex if needed. Existing skill directories are not overwritten.

Scope

The converter preserves submitted claims and proof routes rather than inventing repairs. The audit outputs are model-assisted review artifacts, not machine-checked proofs; inspect their mappings, step findings, dependencies, and unresolved obligations rather than relying only on the headline verdict.

Thanks to Bartosz Naskręcki for introducing the author to Leslie Lamport's original paper on hierarchical proofs and for suggesting that Lamport-style proofs could be useful in AI-assisted mathematical work.

See the README for the worked finite-set example, local checkout workflow, result definitions, and evaluation instructions.