MM0 does not itself do any normalization of expressions. Instead, it acts
as a verification tool for already completed proofs, although it has some
facilities for constructing proofs and it is extensible enough to let you
add more automation to it, which you could use to automate normalization
Hello! if I sound pretentious, it's because I let chat gpt rewrite my
question in better English :). Anyways:
Hello! I've recently stumbled upon formal mathematics due to its potential
application in interactive education. Despite delving into the source code
of mm0 and scanning through
