Two puzzles a day, for the age of machine proofs

Each day draws five claims from the register, balanced across evidence grades so that guessing the commonest grade does not win. Evidence runs from V0, a bare claim, to V3, rebuilt at a pinned commit by someone independent of the authors. Autonomy runs from A1, work done with people, to A3, work the system did alone, and is asked only of claims about a statement itself.

The grades are the register's, set out on the method page. Disagree with one? Every claim links to its full record and its sources.

A Lean proof is only as good as what it rests on. The standard axioms are propext, Classical.choice and Quot.sound. A proof that also depends on sorryAx, on a new axiom someone declared, or on the compiler through native_decide is not a proof on those axioms, whatever its theorem says.

Every snippet in the pool is compiled with Lean, and the axioms it reports are what the game shows. One snippet proves True and calls itself the Riemann hypothesis: it is a genuine proof, and a lesson in fidelity.