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.
