Math was, in principle, fully automated in 1959 (https://en.wikipedia.org/wiki/General_Problem_Solver; the Wikipedia page on its predecessor is better: https://en.wikipedia.org/wiki/Logic_Theorist)

We’re just waiting for hardware engineers to produce faster hardware/software engineers to make the implementation more efficient. ;-)

Having said that, the problems solved here are fairly simple. I can do half of them in my head (how old are the students doing these quizzes?). Getting from the written form to a description that Lean can work with probably is harder than getting Lean to solve them. Skimming the paper, it doesn’t look like they included that first step.

What problem can't be solved, given enough computation power?

For example, determining the 3d description of a photographed scene (a difficult problem) you can just enumerate all the possible scenes, raytrace them, and pick the most probably one (e.g. the one with the simplest description).