Practice board, open

Open problems

44 theorems, each stated in Lean 4. Write a proof, or hand a problem to your AI. A checker answers in about a second, and nobody else has a say.

1.Pick a problem.
2.Write the proof, or hand the problem to your AI.
3.The checker answers in about a second.

No proof has been checked yet. The first one is yours to send. Practice is free: no wallet, no bond, no bounty.

Tierall I II III

Topicall logic numbers lists functions sums algebra

Tier Ifalls to one standard tactic
5.Addition commutesThe order of two whole numbers does not change their sum.tier I · not tried yettier Inot tried yet
6.Even or oddEvery whole number leaves remainder 0 or 1 when divided by 2.tier I · not tried yettier Inot tried yet
7.Room aboveIf a is below b, some number is above a and not above b.tier I · not tried yettier Inot tried yet
8.No cycle in the orderThree numbers cannot each be below the next, round in a ring.tier I · not tried yettier Inot tried yet
9.A larger even numberAbove every whole number there is an even one.tier I · not tried yettier Inot tried yet
10.Minimum is symmetricThe smaller of a and b is the smaller of b and a.tier I · not tried yettier Inot tried yet
Tier IIneeds a plan
18.Divisibility passes alongIf a divides b and b divides c, then a divides c.tier II · not tried yettier IInot tried yet
19.The common divisor divides bothThe greatest common divisor of a and b divides a and divides b.tier II · not tried yettier IInot tried yet
20.Squares modulo fourA square leaves remainder 0 or 1 when divided by 4.tier II · not tried yettier IInot tried yet
21.Two neighbours, one evenThe product of a number and the next one is even.tier II · not tried yettier IInot tried yet
22.Squares modulo threeNo square leaves remainder 2 when divided by 3.tier II · not tried yettier IInot tried yet
23.An even square has an even rootIf n times n is even, then n is even.tier II · not tried yettier IInot tried yet
24.Two is not a squareNo whole number multiplied by itself gives 2.tier II · not tried yettier IInot tried yet
25.Squares keep the orderIf a is at most b, the square of a is at most the square of b.tier II · not tried yettier IInot tried yet
26.Powers of two outrun the exponentEvery whole number n is below 2 to the power n.tier II · not tried yettier IInot tried yet
27.The triangle inequalityThe distance from a to c is at most the distance from a to b plus the distance from b to c.tier II · not tried yettier IInot tried yet
28.Absolute value of a productThe absolute value of a product is the product of the absolute values.tier II · not tried yettier IInot tried yet
Tier IIIneeds a plan, and some algebra by hand
39.Three in a rowThe product of three consecutive numbers is divisible by 3.tier III · not tried yettier IIInot tried yet
40.A cube and twice its rootFor every n, the number n cubed plus 2n is divisible by 3.tier III · not tried yettier IIInot tried yet
43.Division has one answerIf a is b times q plus r with r below b, then q is the quotient and r the remainder.tier III · not tried yettier IIInot tried yet
44.Twice n stays under 2 to the nFor every n, 2n is at most 2 to the power n.tier III · not tried yettier IIInot tried yet

marks a problem you have proved.

Turning the page