Lean4
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.

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.

StatusKind
Not started1. Fizz BuzzstringsarithmeticProgram—Easy
Not started2. Swap a conjunctionlogicconjunctionProof—Easy
Not started3. PalindromestringslistsProgram—Easy
Not started4. Two sumPasslistsarrayssearchProgram—Medium
Not started5. ContrapositivelogicnegationProof—Easy
Not started6. Climbing stairsrecursionperformanceProgram—Easy
Not started7. Valid parenthesesPassstringsstacksrecursionProgram—Medium
Not started8. Gauss’s sumPassinductionarithmeticProof—Medium
Not started9. Count the evenslistshigher-order functionsProgram—Easy
Not started10. An even number above nquantifiersarithmeticomegaProof—Easy
Not started11. Maximum subarrayPasslistsdynamic programmingfoldsProgram—Medium
Not started12. Verified maximumPasslistsspecificationsinductionVerified program—Medium
Not started13. Digit sumrecursionterminationarithmeticProgram—Easy
Not started14. Classical De MorganPasslogicclassicalProof—Medium
Not started15. Fast Fibonacci is correctPassinductionprogram correctnessProof—Hard
Not started16. Run-length encodingPassstringslistsrecursionProgram—Medium
Not started17. Sum of odd numbersPassinductionarithmeticProof—Medium
Not started18. Reversing twicePasslistsinductiongeneralizationVerified program—Hard
Not started19. Insertion sort sortsPasssortinginductive predicatesinductionVerified program—Hard
Not started20. Single numberbit manipulationfoldsProgram—Easy
Not started21. Roman to integerstringspattern matchingProgram—Easy
Not started22. Coin changePassdynamic programmingarraysperformanceProgram—Medium
Not started23. Sum over an appendinductionlistsProof—Easy
Not started24. Best time to buy and selllistsfoldsperformanceProgram—Easy
Not started25. N-QueensPassbacktrackingrecursionProgram—Hard
Not started26. Merge two sorted listslistsrecursionsortingProgram—Easy
Not started27. Divisibility is transitivedivisibilityexistentialsProof—Easy
Not started28. Longest substring without repeatsPassstringssliding windowProgram—Medium
Not started29. No witness means neverPassquantifierslogicProof—Medium
Not started30. Edit distancePassdynamic programmingstringsperformanceProgram—Hard
Not started31. Powers of two grow fastPassinductionarithmeticProof—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.