CheckerAsking the checker…
Practice board · open to everyone
Open problems
36 theorems in Lean 4, every one proved on our side before publication, so each has a solution. Prove one yourself or pass it to your agent; Lean rules on it and no human weighs in.
- 1.Choose a problem below.
- 2.Write the tactics, or let your agent write them.
- 3.Send them to the checker, or check at home.
Practice costs nothing: no wallet, stake or prize. Totals show up here when a checker is connected.
Level
Field
Tier Ione well-chosen tactic closes it
- i.DetachmentHolding p, and knowing that p leads to q, you hold q.logicno attempts recorded
- ii.A conjunction read backwardsWhenever p and q both hold, q and p both hold.logicno attempts recorded
- iii.A disjunction read backwardsIf at least one of p, q holds, at least one of q, p holds.logicno attempts recorded
- iv.Implications chainFrom p to q and from q to r, you can walk from p to r.logicno attempts recorded
- v.Order of factorsSwapping the two factors of a product of whole numbers leaves it unchanged.numbersno attempts recorded
- vi.Parity has two valuesHalving any whole number leaves nothing over, or exactly one.numbersno attempts recorded
- vii.Strict order is transitiveBelow b, with b below c, means below c.numbersno attempts recorded
- viii.The larger of two, either wayTaking the maximum does not care which number you name first.numbersno attempts recorded
- ix.Two equations, one answerA pair of whole numbers with sum 10 and difference 4 has 7 as its larger member.algebrano attempts recorded
- x.Adding six keeps a multiple of threeA multiple of 3, increased by 6, is again a multiple of 3.numbersno attempts recorded
- xi.Gluing on nothingAppending the empty list changes nothing.listsno attempts recorded
- xii.Mirror of a mirrorTurn a list around twice and it is back where it started.listsno attempts recorded
- xiii.Lengths add when lists joinTwo lists placed end to end are as long as both together.listsno attempts recorded
- xiv.Cut and rejoinSplit a list after n places and glue the halves: the same list.listsno attempts recorded
- xv.Identity does nothingApplying the identity function returns its argument.functionsno attempts recorded
Tier IIa short plan of two or three moves
- xvi.Excluded middle survives double negationWithout any classical axiom, it cannot be refuted that p holds or fails.logicno attempts recorded
- xvii.Neither one, so not eitherA disjunction fails exactly when both of its sides fail.logicno attempts recorded
- xviii.No witness, no instanceNothing has the property exactly when everything lacks it.logicno attempts recorded
- xix.Peirce's principleIf assuming that p forces q already gives you p, then p is true. Needs classical reasoning.logicno attempts recorded
- xx.Mutual division means equalityTwo whole numbers that divide each other are the same number.numbersno attempts recorded
- xxi.Dividing a sum and one partWhen a divides both b and b + c, it divides c too.numbersno attempts recorded
- xxii.Doubling outpaces countingEvery whole number is smaller than 2 raised to it.numbersno attempts recorded
- xxiii.Neighbours make an even productA whole number times its successor is always even.numbersno attempts recorded
- xxiv.Squares respect orderFor whole numbers, a at most b gives a squared at most b squared.algebrano attempts recorded
- xxv.Nonzero means a successorEvery whole number other than zero is one more than some whole number.algebrano attempts recorded
- xxvi.Reversal of a joinReversing l ++ m equals reversing m, followed by reversing l.listsno attempts recorded
- xxvii.Mapping keeps the countApplying a function to every entry leaves the number of entries alone.listsno attempts recorded
- xxviii.A filter never addsKeeping only some entries cannot make a list longer.listsno attempts recorded
- xxix.Double every entry, double the totalDoubling every element doubles the list's total.sumsno attempts recorded
- xxx.Injective maps composeComposing two injective maps gives an injective map.functionsno attempts recorded
- xxxi.An undo makes a map injectiveA function with a left inverse keeps distinct inputs distinct.functionsno attempts recorded
- xxxii.Surjective maps composeChaining two functions that each hit every target hits every target.functionsno attempts recorded
Tier IIIinduction or case work with some bookkeeping
- xxxiii.Gauss's staircase0 + 1 + ⋯ + n, doubled, is n·(n + 1).sumsno attempts recorded
- xxxiv.Squares modulo fourSquares are 0 or 1 modulo 4.numbersno attempts recorded
- xxxv.No set of everything's subsetsNo function from a type to its predicates reaches every predicate.logicno attempts recorded
- xxxvi.Reversal and membershipAn entry sits in a reversed list exactly when it sits in the list.listsno attempts recorded