> Obviously Igor is on the right way with theorem cu3addd <https://us.metamath.org/mpeuni/cu3addd.html>.
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). To my surprise mm-lamp works with proofs containing 350 steps (not very fast though, but workable). I feel like I would be able to complete proving 3cubeslem3. 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. > I hope someone will find this little challenge interesting For sure! Before that challenge I never created new proofs. I was only developing my proof assistant and testing it on proofs based on David’s tutorial for mmj2. But this challenge gave me a good starting point and new ideas of what I can add to my proof assistant. > What do you think about having a separate file in the repository with "easier" unproved statements, which do not require new definitions to state or prove? These may serve as a guide on what to do for newcomers (or anyone else), or as a work in progress plan to formalize some big result. I think this is a great idea. At least that’s what I needed to start doing my new proofs. - Igor On Monday, December 18, 2023 at 8:23:29 AM UTC+1 Thierry Arnoux wrote: > Hi Saveliy, > > The current implementation not only performs matches (that it, > unifications), but also allows you to capture the unification results in > new variables, which can later be reused. > > One of the reason I thought about a scripting language is that I wanted > the core (the language interpreter) to be database agnostic, while the > script themselves could be tailored to a database. But that might also > be realized with a multilayered library (for example, one specific > library using services from another, agnostic, library). A scripting > language also has the advantage that it can be used as an external, > without the need to e.g. recompile for each use. In the end, the > language in which I specify how the tactics are used, can also be used > for writing the tactics themselves. > > Any such tactics language should definitely allow one to implement > operations as developing or simplifying formulas. That's valid for first > and second order logic formulas, but also for algebraic formulas in the > complex numbers, and the abstract level of generic algebraic structures > like groups, rings and fields. Working on numerical expressions, > performing long additions and multiplications, or for example connecting > to an SMT solver, might require the ability to use some custom code. > > > 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. > > _ > Thierry > > > On 17/12/2023 18:00, savask wrote: > > Thierry, that's a cool project, I had no idea it exists. > > > > I took a brief look at the syntax and the currently implemented > > tactics. The "equality" tactic looks very useful, others are a bit too > > technical for me to understand. Correct me if I'm wrong, but it should > > be possible to write a tactic for expanding polynomial expressions, > > and maybe to port Mario's tactic for long addition and multiplication. > > > > I agree that one would need a more powerful language to implement some > > of the more interesting tactics. The "improve" tactic from metamath > > exe seems as one example. > > > > I'm not sure if it's beneficial to come up with your own scripting > > language for tactics, but if I were to use a library to write a > > tactic, I would certainly prefer to have functions from your language > > like matching patterns etc. > > > -- 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/a77e6818-650d-452b-8f86-58e5d8d824f0n%40googlegroups.com.
