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.