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 available documentation, I find it challenging to fully grasp certain concepts. I'm curious about how mm0 handles the normalization/canonicalization of expressions, if it addresses this at all. My interest stems from its potential use beyond proof generation, particularly in interactive scenarios where users may answer questions. Instead of requiring users to generate entire proofs to demonstrate their abilities, the idea is to allow users to generate expressions appearing in the proof. The backend then determines whether that is sufficient to conclude that the user has proven the provable, thereby eliminating the need to learn the advanced syntax of proof generation software. The concept involves representing questions as provable theorems within mm0 using eroteric logic. For example, a simple "or" question could be answered by "proving" (providing selected expressions to) a theorem: -- Or Inquiry provable sort ef; -- question term askOr: wff > wff > ef; axiom inferOrAnswer1 (a b: wff): $ a $ > $ askOr a b $; axiom inferOrAnswer2 (a b: wff): $ a $ > $ askOr b a $; theorem isExample (h: $ a -> b -> c $): $ askOr (~((a -> b) -> (a -> c))) ((a -> b) -> (a -> c)) $ = '(inferOrAnswer2 (a2i h)); Some questions only require providing an expression to conclude that the end user has likely proven a provable, such as questions about solutions to equations. Tackling this is obviously challenging. How would one approach it, and does mm0/metamath already implement tools that could be useful to compare input expressions for "semantic equivalence"? -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8fdc51fa-a68b-44af-9c6c-6a7aa68cada5n%40googlegroups.com.
