A tip I have to give: the manual says not to work in the prover at first - absolutely do. In fact, just starting out is probably the MOST necessary time to work directly in the prover. If you try to work out the proof in advance, without knowing the depths of the system, you'll be taking the express route to Hell. On Friday, September 11, 2020 at 4:59:11 AM UTC-4 ginx wrote:
> Oh I see, I will check out more of the Metamath Zero project, since it > sounds very interesting. > I will check more about Lean though I think I will still do my project on > Metamath. Also, good luck with zero! > Now that I have a more clear direction of where to go, I know better where > to start, so thanks to everyone on the thread. > > El jueves, 10 de septiembre de 2020 a la(s) 08:01:40 UTC-5, > [email protected] escribió: > >> On Thu, Sep 10, 2020 at 5:36 AM ginx <[email protected]> wrote: >> >>> Also, thanks for the very detailed explanation Mario. After reading it, >>> I think I basically boiled it down to just two possibilities: Descartes >>> Rule of Signs, which as you stated should be doable, and the CS route. >>> Though it might require a lot more library building, I think I incline more >>> towards the second option. As Norm stated before, even if I can’t complete >>> an entire proof, it can certainly be useful to work on the libraries to >>> make it happen in the future, and I’m sure my teachers will understand as >>> well (is only bs level dissertation, not a masters one). >>> >>> As to what specific algorithm, I’m really not sure right now. I guess >>> after I manage to do even an extremely simple, equivalent of 2+2=4, one >>> then I’ll see what I can get into. >>> >> That's a good outlook. Even if you never make it past 2+2=4 the library >> building itself could be a paper or two. If you want a simple example, I >> would suggest Euclid's GCD algorithm, as metamath already has a sort of >> pure version of that without the runtime bounds or computational model, so >> all the necessary pure math stuff is already done and all you need to add >> is the CS stuff. >> >>> Kosaraju can be a good option in order to open up the graph theory >>> possibilities in the future. Oh and about the Sieve, I was referring to a >>> specific implementation that reduces the time complexity by increasing the >>> space one: https://cp-algorithms.com/algebra/prime-sieve-linear.html. >>> >>> Also, you also mentioned that you’re working on a framework for >>> correctness proof, would you also include tools for counting number of >>> steps and other elements or just the correctness? Around how much time do >>> you think it will take you? Mostly out of curiosity since I plan on working >>> on the tools myself regardless of the framework. >>> >> Oh, my framework is a pretty massive project. It probably won't be useful >> for your purposes before you are done with your dissertation. Plus it's not >> directly applicable to proofs in metamath (it's a different logical system, >> very similar to metamath but requiring a translation layer). You can read >> about it here -> https://arxiv.org/abs/1910.10703 , or on the various >> posts on this forum about Metamath Zero or Metamath C. >> >> The framework is focused on correctness proofs of real software. As such >> it is a little too concrete for nice proofs of theoretical CS algorithms. >> It could also be extended to support reasoning about runtime but that's not >> on the agenda for now. >> >>> Lastly, I would definitely check out the other tools, at the very least >>> to expand my views on the subject. Which one would you recommend for a >>> beginner? Isabelle is the only one that I checked before Metamath. >>> >> I'm pretty partial to Lean, since I am personally involved in the library >> maintenance there as well. In particular, there is a really great Zulip >> chat room (https://leanprover.zulipchat.com/) about Lean that is very >> friendly (to people of all skill levels) with plenty of smart people and >> mathematicians and me :) . >> >> Mario >> > -- 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/9260ac72-f3ab-4264-ac84-814b1b995bddn%40googlegroups.com.
