LessWrong AI
· Communities
LLMs Are Starting To Noticeably Accelerate Our Work
About a year ago, David and I put up two bounty problems involving natural latents. I am now about 80% confident that both have been resolved, both within the past couple months. Both cases made heavy use of LLMs and Lean.The first to land was Grisha Pochuev's counterexample to the "Existence of a Deterministic Maximal