Introducing myself: Alex Reynaldi

Stream: new members

[Alex Reynaldi]

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]

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]

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]

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

[Fox Thomson]

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]

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]

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]

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

[Mario Carneiro]

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]

but the complexity class P is not defined

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

Oh there was a PR?

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Computability.2C.20P.20.28and.20NP.29/near/208327235

[Alex Reynaldi]

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

Mario Carneiro, Formalizing computability theory via partial recursive functions

[Mario Carneiro]

yes