Comment by DroneBetter

the unit distance problem's paper was human-summarised and condensed significantly from the initial LLM output, so it seems the model did do some theory-building there (possibly providing motivation for the clever trick as a natural deduction, at least in its eyes) before humans cut off all the chaff; I imagine the development was similar here.