block designs

Stream: graph theory

[Johan Commelin]

Has anybody thought about formalizing https://en.wikipedia.org/wiki/Block_design ?

[Yaël Dillies]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Design.20theory.20in.20mathlib4

[Kevin Cheung]

Johan Commelin said:

Has anybody thought about formalizing https://en.wikipedia.org/wiki/Block_design ?

I started working on this. DM me if you are interested.

[Chelsea Edmonds]

In case it is of use/of interest, I did a lot of work on formalising block designs (and related things like Hypergraphs) in Isabelle for my PhD - a starting point would be looking at the AFP entry here: https://www.isa-afp.org/entries/Design_Theory.html. Would be happy to collaborate/be a point of contact for anyone looking to do similar things in Lean.