Wolfram Alpha and ChatGPT
I think ChatGPT is pretty neat but I was somewhat less impressed than everyone else is with the code generation. I actually agree with Wolfram for a change; being human like isn’t always “good”.<p>For example, I asked ChatGPT to give me a proof of Fermat’s Last Theorem in Isabelle&#x2F;Isar.  It quickly gave me some very pretty Isar code, and I was extremely impressed.<p>Until I tried actually inputting it  into Isabelle, and nothing worked. I then started reading the proof, and noticed it was making extremely basic algebra mistakes [1] that even a high schooler would be chastised for. Moreover, I even if I allowed these mistakes with “sorry” [2], the conclusion in the proof didn’t actually follow from the steps.<p>Granted, Fermats Last Theorem is a tricky proof so I understand it struggling with it, but I would have much preferred if it had said “I don’t know how to write proofs in Isabelle” instead of giving something that looks plausible.<p>[1] it seemed extremely convinced that “a^n + b^n = c^n” could be rewritten as “(a + b)^n - c^n = 0”<p>[2] “sorry” in Isabelle basically means “assume this is true even if I didn’t prove it. It’s useful but dangerous.