Comment
Comment by cartoonfoxes
Most definitely. I've been playing with using ChatGPT to generate proof texts in Isabelle/HOL, since it lets me verify the correctness of the output before code generation.
No comments yet
Be the first to share your thoughts.