[isaacfrond]

The proof is here: https://www.overleaf.com/project/69dd1d8437eba662fda82929

[adrian_b]

Much more interesting than the proof would be to see the exact prompts used by Liam Price to generate the proof.

[martin293]

I have no exact prompt to share, but he does write:

> Appreciate the insight! If it's at all of interest, this was a one-shot (supposed) solution in about 80 mins, unlike some other problems like 851 that took over 20 continuations totalling perhaps 15-20 hours of reasoning time.

Source: https://www.erdosproblems.com/forum/thread/1196#post-5365