Zulip Chat Archive

Stream: new members

Topic: Adding DFA regular expression equivalence to mathlib

Russell Emerine (May 01 2022 at 22:15):

Hello y'all, I'm Russell, an undergrad at CMU. I have a working proof of the equivalence of regular expressions to DFAs. I'd like to add my proof to the lean 3 mathlib. How should I start a PR? I'd also like some opinions on how to formulate the key theorems and organize parts of the proofs, more details if anyone asks. Thanks to everyone here for running such an awesome project!

Yaël Dillies (May 01 2022 at 22:33):

Hey! @Fox Thomson and I had work towards it, so please show us so we can compare.

Yaël Dillies (May 01 2022 at 22:33):

Once the @maintainers have given you write access, you will be able to open a PR from the mathlib repo (not a fork).

Eric Wieser (May 01 2022 at 22:36):

(we can't give write access without a github username!)

Bryan Gin-ge Chen (May 01 2022 at 22:52):

Welcome! In case you haven't already seen it, we've got a page with some tips for new contributors: https://leanprover-community.github.io/contribute/index.html

Russell Emerine (May 01 2022 at 23:09):

Sorry, my github is just RussellEmerine

Bryan Gin-ge Chen (May 01 2022 at 23:50):

Russell Emerine said:

Sorry, my github is just RussellEmerine

Invite sent! https://github.com/leanprover-community/mathlib/invitations

Russell Emerine (May 04 2022 at 21:30):

i promise i'm working on this lol, there'll be new stuff in a new branch soon

Russell Emerine (May 05 2022 at 02:18):

Ok, now what I had already is on the branch RussellEmerine/DFA_equivalent_regular_expression. I'll be making some of the more obvious changes soon, please let me know if there's anything in particular that needs to be fixed or reorganized.

Last updated: Dec 20 2023 at 11:08 UTC