Having worked a little bit in Lean and Agda(which is also educational-ish), Lean has all sorts of magical convenience features. For educational proof checker, I

Having worked a little bit in Lean and Agda(which is also educational-ish), Lean has all sorts of magical convenience features. For educational proof checker, I think it would be good to be more clear about things and being more mechanical, have a smaller kernel with lower expressivity of types(have strong normalization, don't have universe polymorphism, Large elimination etc).