[lacker]

When a human solves these problems, you might state a "step" in natural language. Like, "apply a polar transformation to this diagram". But that same single step, if you translate into a low-level DSL, could be dozens of different steps.

For an example, check out this formalization of a solution to a non-geometry IMO problem:

https://gist.github.com/mlyean/b4cc46cf6b0705c1226511a2b404d...

Roughly the same solution is written here in human language:

https://artofproblemsolving.com/wiki/index.php/1972_IMO_Prob...

It's not precisely clear what counts as a "step" but to me this seems like roughly 50 steps in the low-level formalized proof, and 5 steps in the human-language proof.

So, my conclusion is just that I wouldn't necessarily say that a 150-step automated proof was inelegant. It can also be that the language used to express these proofs fills in more of the details.

It's like the difference between counting lines of code in compiled code and a high-level language, counting the steps is really dependent on the level at which you express it.