Getting Started with ZeroProofML v0.7.0a1 (SCM)

Install

Create a virtual environment, then install a backend extra:

python -m venv .venv
source .venv/bin/activate

# PyPI install
pip install "zeroproofml[torch]"

# scientific benchmark harness
pip install "zeroproofml[benchmarks]"

# optional experimental plotting/logging utilities
pip install "zeroproofml[viz]"

# optional interactive training-log reports
pip install "zeroproofml[interactive]"

# or, from a repo checkout (development):
# pip install -e ".[dev,torch]"

The zeroproofml[benchmarks] extra installs the NumPy / Torch runtime dependencies used by python -m zeroproofml.benchmarks .... The zeroproofml[torch] extra installs PyTorch for layers, training, strict inference wrappers, and export workflows; the v0.6.x compatibility floor is torch>=1.12. The extra is not platform-empty on Linux, Windows, macOS x86_64, or macOS arm64. The zeroproofml[viz] extra installs optional experimental reporting helpers (zeroproofml.utils.viz, TensorBoardLogger, and jsonl_to_dataframe) in addition to the stable JSONL logger. For dashboard/CSV/BI pipelines, zeroproofml.utils.logging also exposes experimental metric_log_records_to_wide_rows(...) and metric_log_records_to_long_rows(...) converters. The optional zeroproofml[interactive] extra installs Plotly so training-log report regeneration can also write an interactive <stem>_REPORT.html beside the Markdown summary and SVG.

zeroproofml is the canonical public namespace for package/docs/install references. The legacy zeroproof import path is a deprecated compatibility namespace, so existing integrations have a bounded migration window. Compatibility imports remain available through the 0.8.x line; removal is permitted no earlier than 1.0.0 after a documented migration window. See 33_namespace_guide.md for import guidance, maintainer layering rules, and example consistency expectations.

Quickstart

from zeroproofml.scm.ops import scm_add, scm_div
from zeroproofml.scm.value import scm_assert_exact_real, scm_bottom

x = scm_assert_exact_real(3.0)
y = scm_assert_exact_real(0.0)

print(scm_div(x, y))   # SCMValue(⊥) — absorptive bottom on division by zero
print(scm_add(scm_bottom(), x))  # SCMValue(⊥) — bottom absorbs addition

This legacy scalar example asserts exact algebraic literals. In the typed SemanticResult/ResultTensor APIs, raw 0 and 0.0 are only machine observations; exact bottom requires certified PROVEN_ZERO evidence.

Projective vs. Strict SCM

  • SCM mode (default): All operations propagate ⊥ according to meadow axioms. Gradient policies shape backpropagation near singularities.
  • Projective mode (optional): Rational heads run on homogeneous tuples (N, D) during training for smooth optimisation; decoding back to SCM introduces ⊥ only at the boundary.

What Changed from v0.3

  • No Transreal tags (+∞, −∞, Φ); a single ⊥ represents all singular states.
  • Guard logic has been removed—one SCM check at the output replaces layer-by-layer conditionals.
  • Gradient handling is explicit via policies (clamp, project, reject, passthrough) defined in zeroproofml.autodiff.policies.

Next Steps