Refutation and counterexample
A false claim is rejected with a concrete counterexample, which the kernel checks too.
An equally clear answer the other way
When a claim is false, Slean does not answer “not proved”. It looks for one specific configuration on which the quantity changes, and the kernel checks that computation. A refutation is therefore as reliable as a proof.
An example
Claim: “in rule 30, the number of black cells never changes”. Take a ring of 3 cells with a single black cell.
The smallest counterexample
- cell 1 reads
100 → 1 - cell 2 reads
001 → 1 - cell 3 reads
010 → 1
After one step, all three cells are black. The number of black cells goes from 1 to 3. The claim is false, and this ring of 3 cells is the witness.
In Lean
theorem rule30_refuted :
¬ Conserved (eca 30) (tableFn 2 [0, 1]) 1 :=
not_conserved_of_witness _ _ 1 [0, 0, 1]
(by decide) (by decide +kernel) (by decide +kernel)The theorem not_conserved_of_witness says: if one concrete configuration has its total change in one step, then the quantity is not conserved. The three final checks confirm that the world has at least one state, that the configuration is valid, and that the two totals differ.
Why it is useful
- A false proposal costs one proposal from the budget, and it leaves a trace: the refutation goes into the library.
- An agent that proposes at random piles up refutations, and the measurement sees it. See Measuring a discovery.
- Refutations are published alongside successes. That is one of the measurement rules.
The detailed example is on the page A refuted law.