Lean, sunflowers, and circuits

Stream: new members

[Gülce Kardes]

Hello, I am a PhD student in theoretical computer science working on computational complexity, and I’m interested in formalizing a circuit complexity lower bound result which was achieved through an elegant reduction to a combinatorial problem involving the sunflower lemma.

I have searched for existing results on circuit complexity in Lean, as well as more general resources related to the sunflowers, but haven’t found anything. From what I can tell, this community has a few threads from a couple of months ago discussing complexity results, but I’m not sure if there has been any concrete progress since then. Could someone with more expertise confirm whether this is accurate or point me to any useful resources related to Lean and complexity, or Lean and sunflower-lemma type results, so I can get a better sense of where to begin? I’m new to Lean but have experience with Coq. Thank you very much for your time (and very grateful for this Zulip community).

[Shreyas Srinivas]

There is really nothing much in circuit complexity.

[Shreyas Srinivas]

You could formalise the sunflower lemma independently though

[Shreyas Srinivas]

There aren't many theoretical computer scientists from algorithms and complexity in the community in general for now. I hope this changes.

[Shreyas Srinivas]

EDIT : The Isabelle AFP has a recent proof of the sunflower lemma: https://www.isa-afp.org/entries/Sunflowers.html

[Yaël Dillies]

We already tried formalising the (improved) sunflower lemma two years ago and it failed because of holes in the write-up we were following. I think these have been patched since, so it's definitely something you could try!