Suppose I directed some llm agents to factor the primes from network logs of your machine. I then publish the private and public key in full. You would not change your keys of course because its not true right?
My argument is that LLM generation and a correlated Lean verification are not sufficient conditions. Both are falliable.
My argument is that LLM generation and a correlated Lean verification are not sufficient conditions. Both are falliable.