A proof for 3cubes is ready - https://github.com/expln/metamath-theorems/blob/master/metamath-christmas-challenge-2023/metamath-christmas-challenge-2023.mm
- Igor On Monday, December 18, 2023 at 4:59:54 PM UTC+1 savask wrote: > 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/8a6224c7-2db0-4a5b-9c37-a1dd7601cac6n%40googlegroups.com.
