Remix.run Logo
compounding_it 2 days ago

Because the verification would also be done by something non deterministic and then that’s a paradox.

daishi55 2 days ago | parent [-]

Feed the LLM output into a “deterministic” verifier, problem solved. That’s how LLMs verify their new mathematical proofs with lean.