[Tainnor]

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

[est]

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

[mkl]

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