Lean 4 · Problems

Solve problems. Lean checks every step.

Programs, proofs and verified code, judged by the Lean compiler: programs run against hidden tests, and proofs are accepted only when Lean checks every step. Core library only, no Mathlib.

Study paths

Start here5 problems

Five short problems: a program, a proof, a definition to unfold, a string, and a first verified function.

Start: Fizz Buzz

Proofs about programs6 problems

Unfold, simplify, split on cases and finish the arithmetic: the tools of the Academy course of the same name.

Start: Doubling gives an even number

Logic and quantifiers7 problems

From swapping a conjunction to Cantor’s diagonal argument, including the classical steps.

Start: Swap a conjunction

Verified programs8 problems

No tests, only specifications: write the function and prove it correct for every input.

Start: Verified membership test

Induction6 problems

Sums, powers and lists, then strong induction for prime factors.

Start: Sum over an append

Classic algorithms10 problems

The interview classics in Lean, with hidden tests sized so that slow solutions run out of time.

Start: Missing number

Read every problem without an account. Create a free account to run solutions, track what you have solved and join the leaderboard. Easy problems, the daily problem and one Medium a week are free, and the Academy Pass opens the rest.

Kind

1. Fizz BuzzstringsarithmeticProgram—Easy

2. Swap a conjunctionlogicconjunctionProof—Easy

3. PalindromestringslistsProgram—Easy

4. Two sumPasslistsarrayssearchProgram—Medium

5. ContrapositivelogicnegationProof—Easy

6. Climbing stairsrecursionperformanceProgram—Easy

7. Valid parenthesesPassstringsstacksrecursionProgram—Medium

8. Gauss’s sumPassinductionarithmeticProof—Medium

9. Count the evenslistshigher-order functionsProgram—Easy

10. An even number above nquantifiersarithmeticomegaProof—Easy

11. Maximum subarrayPasslistsdynamic programmingfoldsProgram—Medium

12. Verified maximumPasslistsspecificationsinductionVerified program—Medium

13. Digit sumrecursionterminationarithmeticProgram—Easy

14. Classical De MorganPasslogicclassicalProof—Medium

15. Fast Fibonacci is correctPassinductionprogram correctnessProof—Hard

16. Run-length encodingPassstringslistsrecursionProgram—Medium

17. Sum of odd numbersPassinductionarithmeticProof—Medium

18. Reversing twicePasslistsinductiongeneralizationVerified program—Hard

19. Insertion sort sortsPasssortinginductive predicatesinductionVerified program—Hard

20. Single numberbit manipulationfoldsProgram—Easy

21. Roman to integerstringspattern matchingProgram—Easy

22. Coin changePassdynamic programmingarraysperformanceProgram—Medium

23. Sum over an appendinductionlistsProof—Easy

24. Best time to buy and selllistsfoldsperformanceProgram—Easy

25. N-QueensPassbacktrackingrecursionProgram—Hard

26. Merge two sorted listslistsrecursionsortingProgram—Easy

27. Divisibility is transitivedivisibilityexistentialsProof—Easy

28. Longest substring without repeatsPassstringssliding windowProgram—Medium

29. No witness means neverPassquantifierslogicProof—Medium

30. Edit distancePassdynamic programmingstringsperformanceProgram—Hard

31. Powers of two grow fastPassinductionarithmeticProof—Medium

32. Valid anagramstringssortingProgram—Easy

33. Cantor’s diagonal argumentPasslogicsetsclassic theoremsProof—Medium

34. Binary searcharrayssearchperformanceProgram—Easy

35. Merge intervalsPasssortinglistsperformanceProgram—Medium

36. Verified membership testlistsspecificationsinductionVerified program—Easy

37. Longest common prefixstringsfoldsProgram—Easy

38. Number of islandsPassgridsgraph searcharraysProgram—Medium

39. The drinker paradoxPasslogicquantifiersclassical logicProof—Medium

40. Longest increasing subsequencePassdynamic programminglistsarraysProgram—Medium

41. Trapping rain waterPasslistsprefix scansperformanceProgram—Hard

42. Infinitely many primesChallengePassnumber theorystrong inductionclassic theoremsProof—Hard

43. Every number has a prime factorPassnumber theorystrong inductionProof—Hard

44. The square root of 2 is irrationalChallengePassnumber theorystrong inductionclassic theoremsProof—Hard

45. Insertion sort is correctChallengePasssortinginductive predicatespermutationsVerified program—Hard

46. Doubling gives an even numberarithmeticunfoldomegaProof—Easy

47. Clamp never goes below the boundconditionalsunfoldomegaProof—Easy

48. What comes before redcasescontradictioninductive typesProof—Easy

49. A nonempty list has a first elementlistsoptioncasesProof—Easy

50. Verified maximum of two numbersspecificationsconditionalsomegaVerified program—Easy

51. Verified distance between numbersspecificationsconditionalstruncated subtractionVerified program—Easy

52. Missing numberlistsarithmeticfoldsProgram—Easy

53. Reverse the wordsstringslistsProgram—Easy

54. Verified count of occurrencesPasslistsspecificationsinductionVerified program—Medium

55. Majority elementPasslistsfoldsperformanceProgram—Medium

Proof

The statement is fixed and you write the proof. The judge accepts it only when Lean closes every goal without sorry or extra axioms.

Program

Write a function in Lean. Run it against the examples and your own inputs, then submit it against hidden tests, some sized so that slow algorithms run out of time.

Verified program

There are no tests: you prove that the code meets a specification, so it is correct for every input, not just the ones someone thought of.