Check it yourself.

211 proofs, checked in Lean 4.

211 theorem statements about the maths behind Sentinel’s thinking: probability, timing, information, evidence and when to interrupt. Lean checks every step, and an audit confirms none of them rely on a shortcut (no sorry, no extra axioms beyond Lean’s standard three).

Run it

# download sentinel-proofs.zip from the link below, then:
unzip sentinel-proofs.zip && cd sentinel-proofs
lake exe cache get      # downloads prebuilt Mathlib v4.24.0
sh check-proofs.sh      # builds every proof, then runs the axiom audit

Needs Lean via elan. The toolchain is pinned to Lean 4.24.0 and Mathlib v4.24.0.

Files

• sentinel-proofs.zip: the whole Lean project (or browse the source)
• Theorem index: every theorem, what it says and what it assumes
• What wasn’t proved: 77 claims from the notes that were left out on purpose, and why
• Recorded run, 29 October 2026: build log, axiom audit, toolchain, file hashes (its paths start with lean/; in the zip that folder is sentinel-proofs/)

Checked again

On 11 November 2026 the published files matched the 29 October hashes, all 22 of them. Then every proof was built from scratch from these files with Lean 4.24.0: all 211 checked, and the axiom audit came out identical to the recorded one.

What it doesn’t show: each proof is about a specific piece of maths under the assumptions written in its statement. It doesn’t prove the whole mind works, and some of the 211 are small helper steps or standard results restated, rather than separate discoveries.

The simulations.

Three simulated tests, each with a fixed random seed, so the same code gives the same numbers on any computer.

Keeping up with what you’re doing: 92.3%

24,000 simulated moments where a person’s goal kept changing without warning. On the last 10,000, which nothing was tuned on, Sentinel’s method tracked the current goal 92.3% of the time. The best simple method managed 86.7%.

python3 sentinel-personal-significance-experiment.py

Script · recorded output. Standard Python only, under a second.

Learning when to speak up: 2×

24 fresh simulated worlds, 3,200 possible messages each, under eight conditions. Pacing messages took their usefulness from 62 to 132 per 1,000 against a fixed rule. When each world had its own hidden preferences, learning from feedback took it from 89 to 173.

pip install numpy
python3 sentinel_interrupt_learning_experiment.py --stage heldout --worlds 24 --events 3200

Script · recorded output · summary. About 25 seconds.

A memory trace that tied: 0.925 vs 0.924

Three hidden activities over 15,000 moments. On 5,000 unseen ones, the memory trace scored 0.925 and a simple 13-action history scored 0.924. It didn’t beat the simple method, and that’s the result.

python3 sentinel-relevance-from-experience-test.py

Script · recorded output. Standard Python only.

Checked again

On 11 November 2026 all three were run again from these files. The first two gave output identical to the recorded files, byte for byte. The third matched in everything except the time it was run.

What they don’t show: these are worlds I designed, and the methods were set up knowing how those worlds work. They show the maths does what it should, not that it knows what a real person wants. In ordinary worlds, a well-paced rule that never learned did best, so learning isn’t claimed there.

Real sound, rebuilt perfectly. Word gaps failed.

Sentinel’s ears bet on the sound 10 ms ahead and keep only what they got wrong. From 42 one-minute recordings of my room, 119,943,680 samples, they rebuilt every sample from the bets and misses alone with 0 wrong, using about 1% of one processor core. The same test failed at finding the gaps between words: 56.6% against a placebo’s 51.6%, when it needed 65%.

Why it’s self-reported

The recordings are of my room, so they stay private. The hearing code is part of the app and isn’t public yet.

What you can read

• The rules, written before any code, with what counts as a pass and what kills the idea
• The settings, frozen before the test, with hashes of the code that ran
• The result, including the fail and a bug the test found

Checked again

On 11 November 2026 the hearing code’s own checks were built and run: 90 passed, 0 failed. One of them rebuilds loud, silent and clipped sound exactly from the bets and misses. That only shows the method on made-up sound, not the 42 recordings.

One thing you can check: the result names the SHA-256 of the rules and the settings it ran under, and the two files here match them exactly (001f8186… and 8da4bf4d…). Each file’s page shows its hash.

The dates and times in these files come from my own notes, and the files aren’t under version control, so nothing outside proves the rules were written before the test.