feat(Other): Large Steiner Systems

[franzhusch]

Formalizes the question for a construction of a Steiner System under certain constraints, from https://epoch.ai/frontiermath/open-problems/large-steiner-systems.

Formalization done with the help of Opus 4.6

[mo271]

Thanks, looks pretty good, but I think we should make it a bit more general, also to open it up more towards related problems about Steiner systems.
in Erdős Problesm 835 some comments mention that, that might potentially be another TODO to related the statement there (but if at all in a differenc pull request)

[mo271]

let's move to Wikipedia, use that as a main reference
https://en.wikipedia.org/wiki/Steiner_system

and also use their notation (including creating the S(t, k, n) as lean notation), which is

Do mention this very specific question (with reference to FrontierMath) which is now under large LargeSteinerSystemWitness, with those specific constraints.
But also the known results for t = 5.
and also "also whether infinitely many have t = 4 or 5." (fine to leave those additional questions as TODO if this is too much
Nice to have an example, if it also include the question at least for t = 5 (perhaps mention the Witt design(s)?)

[franzhusch]

Does it really make sense to add it the t=5 case? Because this is about a witness / construction it would really only test if it was in the training or not? Or if he can just find it on the internet. Thats why I have not included it.

[mo271]

One could use ∃! here, but then native decide wouldn't work, I think. If that is the case, let's add a comment explaning this design choice ("we avoid using ∃! in order to stay decidable" or something to that effect)

[franzhusch]

It would indeed break (native) decide, I have left it as a comment.