> 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/071167ef-ea85-4155-919b-09303e6b8f23n%40googlegroups.com.
