Ask HN: Will an AI be able to prove Fermat's last theorem? When?

Do you think an AI will ever be able to correctly answer a prompt like: "Prove Fermat's last theorem in a rigorous way. Produce a proof that can be checked by Coq, Isabelle, Mizar, or HOL in a format supported directly by any of them" and have its output really work and prove it? If so when?