Zulip Chat Archive

To write relevant lean modules containing the basic definitions, results in (Generalised probabilistic theories) GPTs and tools for reasoning about computational complexity in GPTs.

Eric Wieser (Oct 04 2023 at 17:53):

@Jayavishnu R, @Vaisakha Ashok, what is going on here? Is someone teaching a course on computation complexity with Lean?

Jayavishnu R (Oct 04 2023 at 18:00):

@Eric Wieser not exactly

Jayavishnu R (Oct 04 2023 at 18:02):

It was a problem question in a competition

Eric Wieser (Oct 04 2023 at 18:02):

Is the competition public?

Jayavishnu R (Oct 04 2023 at 18:02):

My professor also reacted badly

Jayavishnu R (Oct 04 2023 at 18:03):

Jayavishnu R (Oct 04 2023 at 18:06):

@Eric Wieser not exactly

Eric Wieser (Oct 04 2023 at 18:08):

If it's public, can you provide a link to information about the competition?

Eric Wieser (Oct 04 2023 at 18:39):

Resolved privately; this is a problem from https://www.sih.gov.in/, with description

Lean module for reasoning about computational complexity in GPTs.

Formalization of mathematics and computer science is in vogue. Formalization means to express mathematical concepts, definitions, theorems, and proofs in a way that can be checked by a computer for correctness. Lean theorem prover is interactive and based on dependent type theory which is a powerful and expressive framework for formalizing computer science. It has been used for example in formalization of number theory. Similarly, it can be used to formalize the notion of computational complexity of generalized probabilistic theories (GPTs). Some of the relevant computational complexity classes are BGP (=AWPP), BQP, BPP, PP, PSPACE. We can formalize the notions of these computational complexity classes and the relations among them in lean. We can also move further on to formalize the notion of higher order interference in physical theories and formalize some theorems related to it. The exact problem is to write relevant lean module(s) containing the basic definitions, results in GPTs and tools for reasoning about computational complexity in GPTs. The developed module can further be used to give formal proofs for theorems and lemmas.

Organization: Ministry of Defence

Martin Dvořák (Oct 04 2023 at 18:44):

If somebody develops that Lean module, it will be abso-bloody-lutely amazing!

Shreyas Srinivas (Oct 04 2023 at 18:57):

Why would any ministry of defense care about computational complexity :surprise:

Shreyas Srinivas (Oct 04 2023 at 18:59):

And they want this in four days. I don't understand the expectations here.

Shreyas Srinivas (Oct 04 2023 at 18:59):

(deleted)

Martin Dvořák (Oct 04 2023 at 19:01):

Da heck? Even if the whole Lean community united on the single project and worked on it with maximum intensity, we wouldn't deliver anything meaningful in four days.

Adomas Baliuka (Oct 04 2023 at 19:05):

Government agencies and grants work in mysterious ways sometimes...

Eric Wieser (Oct 04 2023 at 19:27):

I think maybe they want a proposal/ plan in four days

Shreyas Srinivas (Oct 04 2023 at 19:58):

ab said:

Government agencies and grants work in mysterious ways sometimes...

This is not exactly a grant. It is a hackathon for students, all the way from high school to doctoral students.

Shreyas Srinivas (Oct 04 2023 at 20:00):

I am not sure it is possible to come up with any meaningful proposal to formalise complexity in 4 days. Even in other theorem provers there aren't that many complexity theoretic results and I don't see any consensus on even the model of computation to use.

Shreyas Srinivas (Oct 04 2023 at 20:02):

At least in India, hackathons definitely require a reasonable prototype.

Arunkumar V (Dec 14 2023 at 04:37):

Any tips on how to proceed :pray:

Arunkumar V (Dec 14 2023 at 04:38):

Jayavishnu R said:

To write relevant lean modules containing the basic definitions, results in (Generalised probabilistic theories) GPTs and tools for reasoning about computational complexity in GPTs.

For this statement.

Arunkumar V (Dec 15 2023 at 07:18):

Shreyas Srinivas said:

@_ab|638715 said:

Government agencies and grants work in mysterious ways sometimes...

This is not exactly a grant. It is a hackathon for students, all the way from high school to doctoral students.

Any ideas to implement :sweat:

Arunkumar V (Dec 15 2023 at 07:19):

Martin Dvořák said:

If somebody develops that Lean module, it will be abso-bloody-lutely amazing!

Any tips sir

Shreyas Srinivas (Dec 15 2023 at 15:53):

Arunkumar V said:

Any ideas to implement :sweat:

Sorry, I can't think of anything reasonable one could implement in a hackathon lasting a few days. You could try writing a domain specific language for making it easy to write Turing machines that then compiles into a suitable data structure internally. With enough API lemmas, this should make Turing machine descriptions for proofs easy to write and easy to prove things about. This is only feasible if you know a reasonable amount of lean metaprogramming. I just find the whole challenge that has been put up unrealistic.

Shreyas Srinivas (Dec 15 2023 at 15:56):

You could use it as a chance to test out Lean Copilot

Last updated: Dec 20 2023 at 11:08 UTC