$\mmath$ tools

To achieve its objectives, the $\mmath$ project is made up of several tools with different intended usages in various kinds of math courses. These tools include

  • The formal $\mmath$-language whose syntax and logical foundation is close to common usage in lectures (...details)
  • A proof checker for $\mmath$-texts (...details)
  • A Scala-$\mmath$ library providing data structures for basic mathematical objects (...details)
  • A code generator to build libraries from algorithms written in $\mmath$-language (...details)
  • A sequence of lecture notes which emphasize formal aspects by adopting parts of the $\mmath$-language (...details)

Some of these tools are currently under development, some are still in their planning phase.