Computer Theorem Provers (TP) are becoming ready for industrial use -- and raise demands to educate engineers in "Formal Methods", based on mechanised mathematics, modeling and proving. This demand calls for rethinking mathematics education in general -- and for adapting TPs to educational requirements. Particular educational requirements are: (1) check user input automatically, flexibly and reliably -- TPs are made for proving, and input establishes a proof situation (2) give exhaustive explanations on request by learners -- knowledge underlying TPs is human readable (not program code) (3) propose a next step if learners get stuck -- the greatest challenge for TPs. This talk will relate several TP-based systems to these three requirements and thus give examples for discussion: What are further requirements from education to TP technology? How can TP-based education in proving narrow the gap between high-school math and academic math?