Here are a few videos which show the automation I used to prove some parts of 3cubes (all videos are speechless):
Part 0 - initial setup to make this demo easier to reproduce https://drive.google.com/file/d/1x-cV6dL3wqEeKalbXlaRP7AtZmxnFlWQ/view?usp=drive_link Part 1 - converting a polynomial to the “base form” https://drive.google.com/file/d/1IOk3QMteDB-IyV8OCWS56miyfcXksOFy/view?usp=drive_link Part 2 - proving equality of two polynomials. This part also shows how to automatically create inference and closed forms from an existing deduction form (at the end of the video). Also, in this part, I cut a lot of time where the screen was blinking. So, macros work faster on the video than in reality. https://drive.google.com/file/d/1hipxElyqrkuKYzEjH_AR4c0uap_3MYvu/view?usp=drive_link Part 3 - creating a simple macro https://drive.google.com/file/d/1qpFCZTXXVZ6TwJuuA_OPnAgfXzFiPrAZ/view?usp=drive_link This automation is based on macros. A macro is a JavaScript function which automates one or few manual steps by calling special predefined API functions. Those API functions allow to interact with metamath-lamp functionality (everything works locally, there are no calls via the Internet). Those API functions do something which could be done manually. Only the proveBottomUp API has some additional capabilities not available via the UI. I am not providing more details because this is still a work in progress. This has not been released yet and it is available on dev <https://expln.github.io/lamp/dev/index.html> version of metamath-lamp at the moment. - Igor On Wednesday, January 3, 2024 at 11:02:53 AM UTC+1 Igor Ieskov wrote: > > I agree, Igor, congrats!! > > Thanks, David! > > > I'm hoping that you'll format it so that it (or at least some of the > supporting parts) > > can eventually be moved into the "main" body as well. > > Sure, I will format as required for set.mm. > Anyway, I think my PR will not be merged without appropriate formatting. > > - > Igor > > On Tuesday, January 2, 2024 at 9:44:47 PM UTC+1 David A. Wheeler wrote: > >> Savask: >> >> > > Igor, congratulations! >> >> I agree, Igor, congrats!! >> >> > On Jan 2, 2024, at 12:07 PM, Igor Ieskov <[email protected]> wrote: >> > >> > Thank you! Sure, I will add it into my mathbox after some enhancement. >> >> That's great! I'm hoping that you'll format it so that it (or at least >> some of the supporting parts) >> can eventually be moved into the "main" body as well. >> >> This theorem of Ryley ("every rational number is a sum of three cubes of >> rational numbers") is >> general, so I think it's worthy to eventually be the main body. We often >> put >> things in mathboxes first, then *later* move them into the body, so it'd >> be a pretty typical progression. >> >> > At the beginning I didn’t know what approach to use. That’s why there >> are theorems in different forms in the beginning. Initially I created all >> three forms (inference, deduction and closed) for each theorem because I >> didn’t know what form I would need further in the proof. But somewhere in >> the middle of the proof I realized that I need only deduction. Before >> creating a pull request I will remove all redundant theorems. >> >> I agree. Putting most things in deduction form makes it easier to combine >> results, and you can always create the other forms from deduction form. >> >> > > By the way, did you end up using some automation to finish the proof, >> or you did it all by hand after all? >> > >> > The parts where I needed to compare or transform polynomials have been >> proved in semi-automatic mode. Everything else has been done manually. I >> heavily used the bottom-up prover of mm-lamp, but I count it as “manual >> mode” because it is able to find only very simple proofs. By the >> semi-automatic mode I mean a new automation functionality which I added to >> mm-lamp while working on this proof. It is currently not available on the >> mm-lamp web site, but I will release it in one of the next versions >> (hopefully in the next one). >> >> I'm looking forward to this new automation functionality in >> metamath-lamp! >> >> I think metamath-lamp is a nice proof assistant for Metamath. >> If you're interested in learning more about metamath-lamp, I wrote this >> guide: >> https://lamp-guide.metamath.org/ >> and the first chapters of that guide are also available as videos: >> https://www.youtube.com/playlist?list=PL1jSu6GGefBk3RhHW5Srpc2qxWMqhga9J >> >> Metamath-lamp isn't perfect of course. Its "unification" algorithm >> currently has a known weakness >> (it's really just a "match" algorithm, so sometimes you have to >> hand-execute replacements >> that would be automatic in tools like mmj2 that use full unification). >> That's not fundamental to the tool, it's just a weakness of its current >> implementation. >> In addition, mmj2 has some nice situation-specific automation that >> metamath-lamp currently lacks. >> That said, you can start using metamath-lamp without installing anything >> ("just use your >> web browser"), and it even works well on a mobile phone without >> installing anything. >> That "ease of getting started" makes metamath-lamp a nice addition to our >> collection of tools. >> So congrats to Igor for both the proof *and* for developing the >> metamath-lamp tool! >> >> --- David A. Wheeler >> >> -- 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/c7ae52d9-cb25-4724-a89c-e64e5a13008cn%40googlegroups.com.
