Holy shit, this has to be one of the most difficult proofs to formalize due to it's length and complexity right?

Yep. There may be only 25-50 people alive today in the whole world who can credibly claim to understand Wiles' proof. Now we add an LLM to that list. Absolutely mind-blowing stuff.

▲

simpaticoder 2 hours ago | parent | next [-]

But isn't that understanding discarded? It is if you mean "intermediate working state" while it was generating the LEAN code. Which raises the question: I wonder what other directions it could have gone in those intermediate states? Is it possible to snapshot the state of an LLM (or a cluster of them) "in the middle of proving FLT" and then prompt it to go in a different direction with all that context?

▲

bigstrat2003 an hour ago | parent | prev [-]

> Now we add an LLM to that list.

No we cannot. LLMs do not, by their very nature, understand a single thing. You are giving far too much credence to hype and marketing.

	▲	bjourne 38 minutes ago \| parent [-]
		A meme free of charge for you, sir: https://www.reddit.com/r/singularity/comments/1jl5qfs/its_ju...