You can write "formal" proofs in this language for mathematical theorems. They are "formal" because they are so detailed that they are machine checkable. That's in contrast to the "informal" pen and paper proofs that people normally produce.
Besides pure maths you can also use that to verify the correctness of software. E.g. say you implemented a shortest path algorithm:
shortestPath(graph, start, end)
You could proof something like:
For all `graph` and each `path` in `graph` from `start` to `end`:
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.
Besides pure maths you can also use that to verify the correctness of software. E.g. say you implemented a shortest path algorithm:
You could proof something like: For all `graph` and each `path` in `graph` from `start` to `end`: