TauLib Audit Routes

This page is a hub for the concrete, hands-on routes by which an external reader can audit the TauLib formalization’s claims. Every claim on this site that depends on TauLib is reachable from one of the routes below.

What you can audit, and how

Two-minute audit

For a journalist, reviewer, or specialist who has 120 seconds:

git clone https://github.com/Panta-Rhei-Research/taulib && cd taulib
rg -n '^axiom ' TauLib/                    # expect 3 matches
rg -n ':= sorry' TauLib/                   # expect 0 matches
rg -c 'native_decide' TauLib/ | head        # disclosure: ~1,824 — see /verify/tcb/

If those three checks return what the site claims, the headline TauLib invariants are independently verified. The harder claims (each prediction’s chain through the registry) require the page-level audit routes above.

Where the trust ends and the engineering begins

This audit hub is intentionally short. It is not the verification narrative — that lives at /verify/ and /verify/how-to-verify/. It is the concrete route surface: where to click, what to run, what to grep, when you have decided to inspect rather than read.

For the trust-budget question — what does “machine-checked in Lean 4” actually mean here? — start at /verify/tcb/. For the scope-label question — which claims are formal-only, which are bridged to physics, which are metaphorical? — start at /verify/taulib/scope-labels/ and /verify/filter-rules/.