Seems sensible to me. I'm not sure I have any more insight than anyone else about whether it is a good idea, but I'm certainly in favor of encouraging new contributions as best we can.
On June 6, 2022 3:00:56 PM PDT, Jon P <[email protected]> wrote: >Yeah so this is the sort of thing I would imagine, for perhaps the rust >subreddit https://www.reddit.com/r/rust/ (after asking the mods if it's >ok.) Not sure if it's a good idea, it's an example. > >----------- > >Hello Rustacians! > >metamath [link] is a project for creating computer checkable maths proofs. >The means taking old fashioned pen and paper mathematical proofs and >encoding them in such a way that they can be verified by machine, as some >classic examples we have Pythagoras' theorem [link] and the irrationality >of the square root of 2 [ink]. There are over 40,000 proofs in the database >so far and growing, hopefully one day it can cover all of known mathematics. > >There have also been some interesting projects to use AI to generate maths >proofs, such as Open AIs gpt-f [link] and this AI assisted mathematics may >well be the future. > >Anyway what does this have to do with you? Our community is working on a >new verifier and proof assistant called metamath-knife [link] and it's >written in Rust. And there's a lot of Rust based stuff which we could >really do some help with working on, for instance [not exactly sure what >should go here?] creating a good web UI for it, implementing a VSCode >extension and ... > >The verifier is open source and we're an all volunteer community, so no >money is involved. And so yeah if you're either interested in learning >about the mathematical aspects or would be interested in poking around with >the code and helping with some of the programming stuff come and say hi at >our google group [link] or check out the github repo [link]. We have people >who are very strong on the mathematical side so if you are only familiar >with Rust that's still useful to us. > >Computer readable / formally verified mathematics is extremely powerful and >is a very young a promising field which has a lot to explore for anyone >curious about the future of mathematics. > >Thanks :) > >On Thursday, June 2, 2022 at 2:52:53 PM UTC+1 [email protected] wrote: > >> >> >> On June 2, 2022 4:13:35 AM PDT, Jon P <[email protected]> wrote: >> > >> >If that's helpful I don't mind doing the legwork of >> >writing the posts and finding appropriate places to put them (you have to >> >be sensitive to subreddit posting rules etc). >> >> Well I love the idea and it sounds like you have some ideas for how to >> make it sound appealing (which is perhaps not as self evident as a game but >> which seems potentially doable for a group which is some flavor of >> technical). >> > >-- >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/badaf879-4e00-4c69-9109-54841e60d12an%40googlegroups.com. -- 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/61409978-7601-409B-9A0C-AF7A3E3433AB%40panix.com.
