Thierry, > Maybe I'll have another go at implementing the tactics directly in an (existing) programming language rather than designing a scripting language, and see where this leads me. I'd probably use metamath-knife as a basis for that.
You are definitely exploring new ground here. As far as I understand, most proof systems (like Lean) use one language for proofs and tactics, so they don't have to think about these kinds of problems. I can see how a universal tactic language can be useful though, for one, if it's simple enough, every independent proof assistant could implement some core and immediately get access to all already written tactics for metamath. Igor, > I was able to prove 3cubeslem1, 3cubeslem2 and a bit of 3cubeslem3 in “manual” mode using current capabilities of mm-lamp (I can share proofs if needed). Looks like you're close to proving 3cubes indeed! > ... But it starts feeling like a not proper use of time doing such proofs manually. So, I am going to start working on adding some automation capabilities to mm-lamp. Funny enough, I had a similar experience with metamath. My contribution was very small, but I was surprised how tiring it was to do the most mundane of things, so I thought I would try to make a proof assistant with automation myself. Long story short, turns out making a proof assistant is way harder than making a verifier, so I gave up :-) It would be amazing if some tool, like metamath-lamp, would have basic automation allowing one to prove statements like 3cubeslem3 with ease. -- 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/6ca50fc2-2fbe-49ef-9df5-88c53271a1fbn%40googlegroups.com.
