Join Exercism’s Lean Track for access to 100 exercises with automatic analysis of your code and personal mentoring, all 100% free.
namespace HelloWorld
inductive World where
| earth | mars
def hello (world : World) : String :=
match world with
| .earth => "Hello, Earth!"
| .mars => "Hi, Mars!"
end HelloWorld
Get better at programming through fun, rewarding coding exercises that test your understanding of concepts with Exercism.
Given an alphametics puzzle, find the correct solution.
Solve the zebra puzzle.
Given a person's allergy score, determine whether or not they're allergic to a given item, and their full list of allergies.
Deterministic functions make code predictable, composable and easier to understand.
Encoding rules directly in types makes them self-documenting and invalid states unrepresentable.
Write programs and prove them correct in the same language. Specification is code.
Go beyond testing by mathematically proving critical properties of your code.
Categorizing types into classes provides lightweight, extensible abstraction.
A powerful macro and elaborator framework lets you extend the language to fit your domain.
Every language has its own way of doing things. Lean is no different. Our mentors will help you learn to think like a Lean developer and how to write idiomatic code in Lean. Once you've solved an exercise, submit it to our volunteer team, and they'll give you hints, ideas, and feedback on how to make it feel more like what you'd normally see in Lean - they'll help you discover the things you don't know that you don't know.
Learn more about mentoring
The Lean track on Exercism has 100 exercises to help you write better code.
See all Lean exercises
