> hooking up creative LLMs to reliable verifiers like Lean show that it’s possible to construct systems where the unreliability is suppressed.

You can also have LLMs create these things called "programs" that are written in "code" that result in deterministic outputs when given inputs.

I say this with a bit of snark to highlight the point that both humans and LLMs can write code that is cheaper to run and easy to verify. I'm not saying Lean being used like this is a bad idea, just that it's just one end of the spectrum.