In the last two decades, the World Wide Web has become the universal information source. Search engines can efficiently serve daily information needs due to the enormous redundancy of relevant resources on the web. For educational and scientific information needs, the web functions much less efficiently: Scientific publishing is built on a culture of unique reference publications, and moreover documents abound with specialized structures such as technical nomenclature, notational conventions, references, tables, or graphs.

With the globalisation in education, bridging cultural differences by making course material more accessible and adaptable to individual user needs becomes an important goal. In this paper we attack this goal for the field of mathematics where knowledge is abstract, highly structured, and extraordinarily interlinked. Modern representation formats like our O format allow us to capture, model, relate, and represent mathematical learning objects and thus make them context-aware and machine-adaptable to the respective learning contexts.

Hilbert's concept of formal proof is an ideal of rigour for mathematics which has important applications in mathematical logic, but seems irrelevant for the practice of mathematics. The advent, in the last twenty years, of proof assistants was followed by an impressive record of deep mathematical theorems formally proved. Formal proof is practically achievable. With formal proof, correctness reaches a standard that no pen-and-paper proof can match, but an essential component of mathematics --- the insight and understanding --- seems to be in short supply.

Two tools addressing different aspects of educational mathematical documents have been developed in our research group and presented to the JEM community at previous occasions: SWiM is a semantic wiki for collaborating on such documents, and JOBAD is a framework that allows for reading documents interactively. In this paper, we outline a vision of an integrated educational environment for interactive learning and collaboration. Starting from an overview of the current state of both SWiM and JOBAD, we show how the vision can be achieved by integrating both systems.

We introduce the MMT language, which provides a simple and scalable Module system for the development of Mathematical Theories. MMT permits to encode mathematical knowledge in a logic-neutral representation format that can represent the meta-theoretic foundations of mathematical and logical systems together with the represented knowledge itself and interlink the foundations at the meta-logical level. This ``logics-as-theories'' approach makes system behaviors as well as their represented knowledge interoperable and thus comparable.

Even though OpenMath has been around for more than 10 years, there is still confusion
about the ``semantics of OpenMath''. As the upcoming MathML 3 recommendation will
semantically base Content MathML on OpenMath Objects, this question becomes more
pressing.

One source of confusions about OpenMath semantics is that it is given on two levels: a
very weak algebraic semantics for expression trees, which is extended by considering
mathematical properties in content dictionaries that interpret the meaning of (constant)

OpenMath is a standard for the representation and communication of mathematical objects,
which are built up from symbols and variables using applications, binding expressions,
and key-value attributions. OpenMath2 introduced a set of symbol roles that can be
specified in content dictionaries to restrict the occurrences of the respective
symbols. This yields a simple, high-level notion of well-formed objects.

While this system is appealing in its simplicity, the definition of well-formedness is

This video is based on the talk given by M. Seppälä at the JEM Workshop in Barcelona on June 9, 2009. The video discusses the potential of Real Time Quizzes in class rooms, and describes the TSARQ system, developed by the WebALT Company, which allows the instructor to administer quizzes to which students respond by sending SMS messages with their cellular telephones. This is a very powerful notion, and allows one to integrate Assessment for Learning to instruction in a completely new way. The WebALT Team, Dr. Lebedev, Dr. Caprotti and Dr. Pauna, is responsible for the work presented here.

We present how to set up VLEs to accommodate mathematics learning. We concentrate on the popular open source Moodle platform and introduce input filters to conveniently write and display mathematical formulas. Moreover, we present techniques for doing interactive math questions in Moodle.

Workshop that concentrates on using automatic assessment in mathematics education in various school levels. We introduce the type of content that has been used in high schools, technical engineering schools and universities and different methodologies that are suitable in these environments. We provide teacher guide lines and case studies. We also discuss the new possibilities given by using the automatically graded exercises in mobile phones as quick "clicker" type tests in middle of lectures.