Hacker News Reader

is there a simpler version of LEAN suitable for high school student level math? Sympy?

It's a game implemented in lean, where you work your way through the basic facts about natural numbers.

sympy is not a proof assistant, but a symbolic computer algebra system

Well I'd say it's enough to automatically solve many high-school level problems, automatically. Like a poor man's Mathematica or WolframAlpha.

Yes, but that's a totally different category of problem from what proof assistants do.