Comment by charlieyu1

The biggest problem is LLM tends to produce over engineered, very complicated proofs that are an eyesore even for relatively simple problems. Give it a beautiful Olympiad geometry problem and LLM will tear it apart into ugly algebraic calculations, turns all lines and circles into equations and calculate their intersection points that spans multiple pages because it is a guaranteed way to solve it. Correct, but hardly any use to the user.