Bollobás-Thomason Theorem

Stream: general

[Caleb Bunch]

Hello Everyone, I am completely new to LEAN so forgive me if this is not the best place to ask this question. My advisor and I are thinking about formalizing the Bollobás-Thomason Theorem in LEAN. My question is, how feasible is this given the current state of mathlib? Does mathlib have all of the tools needed to formalize this theorem or is there a lot missing? I noticed, for example, that there does not seem to be a definition for the Erdős–Rényi random graph model in mathlib. I would appreciate any advice. Thanks!

[Ruben Van de Velde]

I see @Yaël Dillies mentioned this theorem once a few years ago

[Yaël Dillies]

Indeed. We were discussing it with Bhavik just now. My current work on binomial random graphs can be found in https://github.com/YaelDillies/LeanCamCombi/tree/master/LeanCamCombi/ExtrProbCombi as well as #28248

[Yaël Dillies]

The status is "There are issues, but a bit of thinking/arguing shall soon unblock everything"

[Bhavik Mehta]

You have the option of making an ad-hoc definition of the ER model, and using that for this theorem, but at this point we're close enough to getting the right definition to mathlib that I don't think it's worth it.

[Yaël Dillies]

@Caleb Bunch, I think this is a very good theorem to work on, modulo the fact that binomial random graphs don't yet have a stable API. What are your deadlines, so that if you choose to work on it I know when I should book some time for it?

[Caleb Bunch]

My advisor and I do not have a hard deadline as we are still new to LEAN and need to spend some time learning it. I really just wanted to know if it was a feasible proof to start formalizing given the current development of mathlib.

[Caleb Bunch]

@Bhavik Mehta Sounds good. I think its probably best to wait for you guys if the ER model is almost complete.

[Caleb Bunch]

@Yaël Dillies @Bhavik Mehta Would it be difficult to define a monotone property? Also, is there a way to use a probability coupling style argument in LEAN that you know of?

[Bhavik Mehta]

In this Lean 3 file from three years ago I defined monotone properties, defined the expectation threshold and threshold, and used the coupling argument to prove monotonicity of the threshold in the probability https://github.com/leanprover-community/mathlib3/blob/sunflower/kahn_kalai.lean

[Yaël Dillies]

A monotone property is literally no more than {P : SimpleGraph α → Prop} (hP : Monotone P). Couplings are more or less hard depending on what conditions you want on them.

[Bhavik Mehta]

But these use the ad-hoc definition of the random model, and it was never upstreamed since I wanted the right definition of the infinite product distribution (which we now have) and the right definition of the random graph (which we nearly have)

[Caleb Bunch]

I see. Thanks for linking the kahn-kalai proof! I will take a look at it.

[Bhavik Mehta]

It is not complete! It was just some early progress towards it :)

[Bhavik Mehta]

Do also bear in mind that Lean 3 is now deprecated, so this file shouldn't be seen as anything more than a rough, outdated sketch!

[Caleb Bunch]

Sounds good. I will keep that in mind.

[Caleb Bunch]

Thanks for your help everyone!