Comment by fidotron

LLMs are inexplicably good at working within any tight feedback loop to coerce the desired solution. This is precisely why proof assistants + LLMs are non intuitively successful.

This is also why they're so good at creating three.js or Blender work when the output is so easily constrained to "Look exactly like that". I recently posted https://www.ambionix.com/blog/introducing-the-czp-1/ on here, and the audio engine in that was developed in that way.

It is true that it would be astounding to find if anyone has seen a LLM produce any useful generalization of anything resulting in a simplification. They seem to have a direct tendency to do the opposite. The brutal reality is humans have also undervalued this capability for a long time (I think the Poincare/Hilbert debate is relevant) to the point we are also taught that generalizations are, generally, bad and wrong.