[Someone]

The only definition I know of is https://en.wikipedia.org/wiki/Formal_language. I also think that is the commonly accepted definition.

Taking that as the definition, this definitely is not the first formal language learnable in 1-2 hours. I would think, for example, that the language consisting of just the empty string is older and learnable in 1-2 hours.

They probably mean something like “formal language used for writing mathematical proofs that is (about) as powerful as Lean”, though.