[jfmc]

Surprisingly it can generate Coq proofs. Unsurprisingly the "proofs" are just hallucinations that look right but make no sense at all. See for example: "coq program that proves that p->q is equivalent to q->p", which produces:

Theorem equiv_pq_qp : forall (p q : Prop), (p -> q) <-> (q -> p). Proof. intros p q. split. - intros p_imp_q q_imp_p. apply q_imp_p. apply p_imp_q. assumption. - intros q_imp_p p_imp_q. apply p_imp_q. apply q_imp_p. assumption. Qed.

... together with a lengthy and convincing explanation in natural language.

Sophists would be delighted by these mechanized post-truth AI systems.

[andrepd]

That has been my experience for all my attempts of using chatgpt for any programming tasks: ask it something contained in the first stackoverflow answer when you google your prompt, and sure enough it gives you that. But ask it for something slightly more involved and you get something that looks plausible at very first glance but is just pure junk.