3 ms·
This is very similar to Isabelle's Isar [1], except that Isar definitions and theorems can be formally verified. MMathLingua has no doubt a much better present
by robinzfc 5y ago
This is very similar to Isabelle's Isar [1], except that Isar definitions and theorems can be formally verified.
MMathLingua has no doubt a much better presentation layer for mathematics than Isabelle/Isar. This can be improved with a custom presentation layer, see for example rendering of topological groups theory from IsarMathLib [2] written in Isar (disclaimer - my project).
[1] https://isabelle.in.tum.de/Isar/ https://isabelle.in.tum.de/Isar/
[2] https://isarmathlib.org/TopologicalGroup_ZF.html https://isarmathlib.org/TopologicalGroup_ZF.html