> But ask them to enumerate all the intermediate steps required to create a formal direct proof, and it will loose attention and forget important details as they go out of their input window size.

It's interesting how people will comment on LLM capabilities despite clearly not having engaged with frontier models in any meaningful way in a long time

Having models write Lean proofs of mathematical claims is standard operating procedure for any LLM math discovery!