Cristian Guerra · QA Automation · Medellín, Colombia · @criguex

Mathlib controls: changed is not false

Correct, reformulated and broken statements of three theorems Mathlib already proves, checked by Comparator and then by a second route in Lean, with outcomes pre-registered.

How to read this animation: Each row is one registered case. The Comparator column comes from its receipt; the class is recomputed by verify.py from the published logs. The guard lines are copied from the real logs. Author-designed cases; no held-out cases yet.

Open the evidence animation gallery · Download standalone HTML