It's not exactly like a proof assistant because it has a built-in generate-and-test loop: an LLM generates code until the code passes verification. Basically t

It's not exactly like a proof assistant because it has a built-in generate-and-test loop: an LLM generates code until the code passes verification. Basically that's all of AI nowadays: generate-and-test loops. It's like the 1950's all over again.