166 problems · 60 unsolved

Pick one.

Every statement is already formalized in Lean by formal-conjectures. Easy ones are warm-ups with known proofs. Unsolved ones are open research problems.

Unsolved60

PNP NS RH E101 E1020 E1029 E1030 E104 E1107 E1167 E159 E233 E236 E242 E243 E282 E364 E371 E373 E41 E535 E563 E572 E583 E617 E779 E82 E859 E89 E982 Ag Be Br Bc Ca Ct Co Ab Di Eu Fe Ga Gr Ha Hl In Ju Ku Kt La Le Lo Ln Mo Op RH₂ Pi Po Lv Va

Hard30

NS₂ Poi E194 E275 E277 E31 E437 E438 E482 E484 E519 E645 E646 E690 E728 Ao Bk Bo Cr El Go Ja Jc Lg Li Lc Pe Sn Ls Er

Medium38

Cm E1049 E1054 E12 E18 E19 E295 E317 E329 E358 E42 E44 E68 E69 E872 Do Ev Ee Gu Re Rv Ge Mi Ah Ba Ci Cn Au Cw Gt If Ii Jo Mv Pl Rs So Wo

Easy38

RH₃ E107 E1074 E156 E282₂ E287 E36 E361 E366 E445 E448 E602 E80 E90 E937 Ad Ai En Ey Fi Lt Th Tw AG Bh Cc Cl Cg Gc Gm Hd H Jb Jg Ll Ly Sc Sa

Open · sorry Known result Worker on it Proved here

16 shown

Doubling distributes over addition
theorem two_mul_add (a b : Nat) : 2 * (a + b) = 2 * a + 2 * b
medium
Every natural number is even or odd
theorem even_or_odd (n : Nat) : n % 2 = 0 ∨ n % 2 = 1
medium
Every power of two is positive
theorem two_pow_pos' (n : Nat) : 0 < 2 ^ n
medium
Gauss's formula, doubled
theorem gauss_sum (n : Nat) : 2 * ((List.range (n + 1)).foldl (· + ·) 0) = n * (n + 1)
medium
Remainders repeat with period seven
theorem mod_seven_periodic (n : Nat) : (n + 7) % 7 = n % 7
medium
Reversing a list twice gives the list back
theorem reverse_reverse' (xs : List Nat) : xs.reverse.reverse = xs
medium
The greatest common divisor of a number with itself is the number
theorem gcd_self' (n : Nat) : Nat.gcd n n = n
medium
The minimum never exceeds the maximum
theorem min_le_max' (a b : Nat) : min a b ≤ max a b
medium
Adding zero on the right changes nothing
theorem add_zero_right (n : Nat) : n + 0 = n
easy
Addition of natural numbers is commutative
theorem add_comm_nat (a b : Nat) : a + b = b + a
easy
An even number leaves remainder zero
theorem double_mod_two (n : Nat) : (2 * n) % 2 = 0
easy
Every number is less than its successor
theorem lt_succ_self' (n : Nat) : n < n + 1
easy
The first eleven numbers sum to fifty-five
theorem sum_range_eleven : (List.range 11).foldl (· + ·) 0 = 55
easy
The length of a concatenation is the sum of the lengths
theorem length_append' (xs ys : List Nat) : (xs ++ ys).length = xs.length + ys.length
easy
Three divides twelve
theorem three_dvd_twelve : 3 ∣ 12
easy
Two plus two is four
theorem two_add_two : 2 + 2 = 4
easy