Mathematics · proofs · software

Repository audit: 27 October 2026

Read side by side

On this page

The audit inspected source revision ef52463dbe47. It verified publication records, repaired navigation, and added a bounded Windows software check. It did not perform a new mathematical proof audit or Lean replay.

Source publication

All 153 component receipts passed configuration binding, file-count, and aggregate SHA-256 record-digest checks. Every one of the 135,805 distinct owned source paths matched its committed Git blob SHA-1 and file mode, with exact path case. There were no missing or mismatched selected files. The inspected repository contained 139,690 files in total.

This verifies content-addressed identity against the import records. It is not a new SHA-256 read of every source blob. Separately, the Windows package check read and verified all 2,254 selected Constructive Repair source files against their SHA-256 receipt.

The scope is the selected GitHub collection. It is not an exhaustive audit of files still in ChatGPT Library or the independent library repositories.

The audit found five generated pages out of sync with the current source manifest: the monograph, experiment, and package indexes, the import-status page, and the contribution index. These pages have been refreshed from the existing records. The original scientific components and their sealed evidence remain unchanged.

The status updater previously refreshed only five of the source-navigation renderer's thirteen pages. It now generates and checks all thirteen, alongside the three completion/status/queue documents. Legacy entry-point detection uses the committed Git tree, so a sparse checkout cannot silently remove links to existing editions, and untracked local directories cannot add them.

tools/check_source_receipts.py provides a repeatable check of the entire selected source inventory. The collection workflow now runs it, checks every maintained status/navigation page, and runs the import/navigation/receipt regression suite. The new checks cover changed source hashes, modes, path case, duplicate paths and IDs, aggregate digests, configuration bindings, totals, and sparse-checkout behavior.

Constructive Repair on Windows

The package guide and fresh evidence record Windows 11 / CPython 3.12.14 acceptance of a locally rebuilt wheel whose seven runtime files match the published source:

This is partial Python qualification. F08 remains open for the unresolved symlink controls and a complete distribution gate. No new Lean result or wider platform support is inferred.

Verification and maintenance

From a checkout with the assessed Git history available:

python -B tools/check_source_receipts.py
python -B tools/update_completion_status.py --check
python -B -m unittest discover -s tools -p "test_*.py"

The local repository regression run passed 21 tests using a writable workspace temporary directory. An initial run could not use the sandbox's default temporary directory. The rerun changed only that location. The new tests and source-record checker do not execute imported research programs.

The earlier GitHub collection check succeeded on the inspected source revision. After this audit was published, run 40549709933 passed all collection, source-receipt, navigation, regression, and formal-tooling checks on commit b137eee65edbe37dbb9246318e93c4398c6ffcec. This run did not execute Lean. Consult the current workflow runs for subsequent commits, and the verification guide for local commands.

Machine-readable audit · Public project statement · Finalization queue