The neatest thing I've found on there so far is the theorem proving abilities. Lesson 3 shows you can input things like (thm (= (+ a b) (+ b a))) and it will return a proof that the sum of a and b is equal to the sum of b and a.