Math was, in principle, fully automated in 1959 (https://en.wikipedia.org/wiki/General_Problem_Solver https://en.wikipedia.org/wiki/General_Problem_Solver; the

Math was, in principle, fully automated in 1959 (https://en.wikipedia.org/wiki/General_Problem_Solver https://en.wikipedia.org/wiki/General_Problem_Solver; the Wikipedia page on its predecessor is better: https://en.wikipedia.org/wiki/Logic_Theorist 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.