Beginner contributing Presburger to Automata Theory?

Stream: new members

[Philipp]

Is there anything in automata theory (my favorite subject of computer science) that I could contribute to Lean as a total beginner?
I see that NFAs, DFAs, regexes and their conversion already exist, so..

What about automatons that can calculate Presburger arithmetic/logic?

https://archive.model.in.tum.de/um/courses/auto/ws2021/slides2021/10-Presburger_Arithmetic.pdf

https://people.mpi-inf.mpg.de/~hillen/documents/6_Presburger.pdf

[Alex J. Best]

I'm quite interested in this, I'm actually working on an implementation with a view to using automata in tactics but it's still quite early stages. Were you interested in that sort of thing or more in the theoretical theory of automata etc

[Philipp]

I'm super new to Lean and formal proofs in general so I only had the theoretical theory of automata in mind.
But using automata in tactics sounds pretty cool, I'd love to hear more about this (even though I can't promise that I would understand)

[Shreyas Srinivas]

Alex J. Best said:

I'm quite interested in this, I'm actually working on an implementation with a view to using automata in tactics but it's still quite early stages. Were you interested in that sort of thing or more in the theoretical theory of automata etc

This sounds interesting. Is this about implementing some automata based decision procedures in the style of model checking?