Lean 4 · Problems

Solve problems. Lean checks every step.

Programming and proof problems judged by the Lean compiler. Programs run against hidden tests. Proofs are checked step by step, and the judge confirms they rest only on Lean’s standard axioms, so an answer is accepted only when it is actually correct. Every problem uses Lean’s core library alone, without Mathlib.

Read every problem without an account. Create a free account to run solutions, track what you have solved and join the leaderboard. Easy problems and the daily problem 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

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.