Technologies for "Complete, Transparent & Interactive Models of Math" in Education

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.