Here is a new link for the part 3: https://drive.google.com/file/d/1c5t-Nhuy6KX6UmTtEGjXJa-54HFZhp3x/view?usp=drive_link
(the previous link became invalid) - Igor On Monday, January 15, 2024 at 5:07:17 AM UTC+1 Igor Ieskov wrote: > 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/5b14fab3-a465-48f8-9a83-0f771069ad64n%40googlegroups.com.
