4 ms·
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 mil
by vatsachak 1mo ago
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 1mo agophysics is like sex: sure, it may give some practical results, but that's not why we do it
- vatsachak 1mo agoI 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 1mo agomy feel after a lot of experience with agentic haskell at scale has been...no they cannot and maybe the opposite lol