Zulip Chat Archive

Stream: new members

Topic: Introducing myself: Alex Reynaldi


view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.?

view this post on Zulip Kevin Buzzard (Apr 16 2021 at 08:07):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 17 2021 at 08:51):

but the complexity class P is not defined

view this post on Zulip Mario Carneiro (Apr 17 2021 at 08:52):

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

view this post on Zulip Johan Commelin (Apr 17 2021 at 08:53):

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

view this post on Zulip Mario Carneiro (Apr 17 2021 at 08:53):

Oh there was a PR?

view this post on Zulip Mario Carneiro (Apr 17 2021 at 08:55):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 17 2021 at 08:58):

yes


Last updated: May 16 2021 at 22:14 UTC