# Zulip Chat Archive

## Stream: new members

### Topic: Introducing myself: Alex Reynaldi

#### Alex Reynaldi (Apr 16 2021 at 07:22):

Hi, I'm a second-year undergraduate computing student at Imperial College London. I've just started using Lean for doing textbook exercises (tried it on some basic set proofs, hoping to eventually use it for computability theory).

#### Kevin Buzzard (Apr 16 2021 at 07:31):

Hi. I'm at Imperial too. There has been some recent action in mathlib about finite state automata / pumping lemma. I would really like to see a statement of P v NP in mathlib some day.

#### Alex Reynaldi (Apr 16 2021 at 08:06):

Hi, nice to finally meet you. I've heard about you a little bit from talking to JMC students.

I did see some entries about DFAs and NFAs in the documentation - I'd like to try contributing after my exams. Also, what would need to be done to state the P vs NP problem? Is it setting up all the necessary definitions of P, NP, decision problems etc.?

#### Kevin Buzzard (Apr 16 2021 at 08:07):

I'm not the best person to talk to about this. @Fox Thomson ?

#### Fox Thomson (Apr 16 2021 at 09:05):

Hi Alex, I have been working on regular languages but have also taken a bit of a break for exams, I think the next big milestone would be to show that DFAs and regular expressions are equivalent. I would also really like to see statements of P, NP etc. We currently have Turing machines and partial recursive functions however I'm not sure how friendly they would be to complexity theory, maybe we need some different model of computation.

#### Alex Reynaldi (Apr 17 2021 at 08:47):

Fox Thomson said:

Hi Alex, I have been working on regular languages but have also taken a bit of a break for exams, I think the next big milestone would be to show that DFAs and regular expressions are equivalent. I would also really like to see statements of P, NP etc. We currently have Turing machines and partial recursive functions however I'm not sure how friendly they would be to complexity theory, maybe we need some different model of computation.

Thanks for the overview - I'll give it a try as I learn more about lean. Are there any guides/readmes on which constructs I should start looking at? I think I'm looking to start with recursive functions as I've already got some pen & paper proofs for those from doing textbook exercises. I found the mathlib docs to be comprehensive but wasn't sure where to start.

#### Mario Carneiro (Apr 17 2021 at 08:49):

Not really, there's a paper about the library but it's not too detailed about the nitty gritty. But you can ask me if you have any questions about it

#### Mario Carneiro (Apr 17 2021 at 08:49):

I would certainly like to make the turing machine stuff useful for complexity theory, this was one of the goals

#### Mario Carneiro (Apr 17 2021 at 08:51):

The `turing_machine.lean`

file contains 3 or 4 different computational models and (polynomial time) translations between them, and `tm_to_partrec.lean`

constructs a (polynomial time) simulation of partial recursive functions as a TM

#### Mario Carneiro (Apr 17 2021 at 08:51):

but the complexity class P is not defined

#### Mario Carneiro (Apr 17 2021 at 08:52):

I recall someone was working on this, but whatever they did never turned into a PR

#### Johan Commelin (Apr 17 2021 at 08:53):

I think @Pim Spelier and @Daan van Gent made some PRs in complexity theory last year.

#### Mario Carneiro (Apr 17 2021 at 08:53):

Oh there was a PR?

#### Mario Carneiro (Apr 17 2021 at 08:55):

#### Alex Reynaldi (Apr 17 2021 at 08:57):

Just to be sure, this is the paper you're referencing right?

Mario Carneiro, Formalizing computability theory via partial recursive functions

#### Mario Carneiro (Apr 17 2021 at 08:58):

yes

Last updated: May 16 2021 at 22:14 UTC