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/029673b9-fdd9-4376-b81e-284bee9abef4n%40googlegroups.com.
