I believe that's just the definition of the problem.

> theorem main : MainStatement.{u} := by

> sorry

no proof