What's the catch? The video goes into detail, with the AI program using the
Lean proof assistant under the hood. There is an extra program for translating the natural language statements of the problems into a Lean statement, but it isn't reliable, so that was done by a human. The video shows diagrams for the geometry problem.
There doesn't seem to be anything here yet