Check
Split into atoms, each with its evidence.
Each sentence is an atom. Each atom gets a label, the checker that settled it, and a SHA-256 receipt over the claim, the label, the check and its output.
Try one:
Atom
Settled by
This runs the site's checker engine in your browser, the same code as the home page's box and the MCP tool check_claim: finder.js finds the math in each sentence, checker.js settles it with exact fractions, unit tables, rounding bounds and primality, and public_check.js matches the Atlas facts word for word. Anything else returns NOT CHECKED with the reason, never false. Nothing you paste leaves the page.
Label rules
How each label is earned.
| Label | Rule | Evidence kept | Rerun |
|---|---|---|---|
| Proven | A machine proof the Lean 4 kernel accepts, with no sorry and no new axioms. | Source, toolchain version, proof hash | lake build |
| Measured | The arithmetic is proven; the inputs come from a named measurement within its stated uncertainty. | Source, value, uncertainty, unit trace | Recompute script |
| Reasoned | Follows from Proven or Measured facts by an explicit chain; any gap is named. | The chain, link by link | Read the chain |
| Guess | None of the above holds yet. | What is missing | None |