Kai-Kalai conjecture

Stream: maths

[Patrick Massot]

Should we try to formalize https://arxiv.org/abs/2203.17207? It is covered in https://www.quantamagazine.org/elegant-six-page-proof-reveals-the-emergence-of-random-structure-20220425/

[Yaël Dillies]

branch#kahn_kalai

[Yaël Dillies]

@Thomas Bloom and I were thinking about this when the paper came out on Arxiv.

[Patrick Massot]

Great!

[Jineon Baek]

Any progress on this? I am reading the Park-Pham proof of the Khan-Kalai conjecture now, and this seems to be a good one to formalize.

(I initially searched "Khan-Kalai" and it didn't give this thread as the spell was wrong; now it should be OK)

[Yaël Dillies]

@Bhavik Mehta led a project on it two years ago. It didn't go very far

[Yaël Dillies]

There might be progress next week as comb2024 will include both a series of lectures about the Kahn-Kalai conjecture and related problems AND a workshop on formalisation by Bhavik.

[Bhavik Mehta]

The main barrier is still a good formulation of probability for combinatorics. I have a branch on mathlib 3 which starts this, and it was attempted again later in LeanCamCombi, but I believe that aspect has since stalled

[Bhavik Mehta]

I'm not quite sure which project you're referring to, @Yaël Dillies, could you elaborate?

[Bhavik Mehta]

(deleted)

[Yaël Dillies]

At Kevin's workshop, September 2022?

[Bhavik Mehta]

No, that was on sunflowers not Kahn-Kalai, and it got stuck because the proof we were following had some difficult to fix errors. The proof ideas have a vague similarity but the formalisations are disjoint.

[Yaël Dillies]

Ah right

[Violeta Hernández]

Bhavik Mehta said:

The main barrier is still a good formulation of probability for combinatorics.

Is there an issue with just specializing the general definition from measurable spaces?