Can Formal "Solver Loops" Make LLMs Actually Reason? Four Mathematical Proposals — LessWrong