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/CAFXXJSsjGNh8Zd1BdT1LV4U6bC6nkFTp%3DN2yHzO%3DOtOsC2cUnw%40mail.gmail.com.
