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/06ED1B45-4C8F-4551-A60D-EE8116DE4ED6%40dwheeler.com.
