This is quite useless actually. The whole point of formalizing FLT was to clean up modern number theory into reusable abstractions that prove it.

If its 13 million LoC, it might involve so much spaghetti that its unusable other than the result

▲

The_Blade an hour ago | parent [-]

physics is like sex: sure, it may give some practical results, but that's not why we do it

▲

vatsachak an hour ago | parent [-]

I mean at this point there's no doubt that LLM cans be RL maxxed and give you _some working output_ but the next frontier is whether they can create good abstractions, a.k.a use the correct level of expressivity so as to not inline everything yet not play code golf.

	▲	whateveracct 21 minutes ago \| parent [-]
		my feel after a lot of experience with agentic haskell at scale has been...no they cannot and maybe the opposite lol