  A new generation of educational mathematics software is being shaped in ThEdu
and other academic communities on the side of computer mathematics. Respective
concepts and technologies have been clarified to an extent, which calls for
cooperation with educational sciences in order to optimise the new generation's
impact on educational practice. The paper addresses educational scientists who
want to examine specific software features and estimate respective effects in
STEM education at universities and subsequently at high-school. The key
features are characterised as a "complete, transparent and interactive model of
mathematics", which offers interactive experience in all relevant aspects in
doing mathematics. Interaction uses several layers of formal languages: the
language of terms, of specifications, of proofs and of program language, which
are connected by Lucas-Interpretation providing "next-step-guidance" as well as
providing prover power to check user input. So this paper is structured from
the point of view of computer mathematics and thus cannot give a serious
description of effects on educational practice -- this is up to collaboration
with educational science; such collaboration is prepared by a series of
questions, some of which are biased towards software usability (and mainly to
be solved by computer mathematicians) and some of which are biased towards
genuine research in educational sciences.
