In a day or so, the mathematicians behind the #1stproof challenge at https://1stproof.org/ will reveal their solutions to the 10 challenge problems they posted recently. (I am not directly involved in this challenge, although I know most of the authors personally and approve of their experiment.) It seems likely that there will be many claims, both trustworthy and dubious, of proofs of these problems by various AI-generated means.

The Erdos problem web site, having dealt with this type of thing for several months now, has come up with several guidances on how to increase confidence in the correctness of an AI-generated proof: https://github.com/teorth/erdosproblems/wiki/I-think-I-managed-to-get-my-favorite-AI-tool-to-solve-an-open-Erd%C5%91s-problem!--What-do-I-do-next%3F The wording there is specific to Erdos problems, but much of the advice can be applied more broadly.

I would like to highlight in particular the additional correctness guarantees provided by formalizing the argument in Lean. When used correctly, a Lean formalization of a proof can provide extremely high confidence that a given proof correctly proves the desired claim. However, if the Lean proof is itself AI-generated without supervision from an expert in Lean, there are still ways in which a supposed "Lean certificate" of correctness is unsatisfactory or even worthless. These include:

1. A Lean proof that adds additional axioms in the proof beyond the standard three, or which relies on malicious metaprogramming.
2. Subtle errors in the formalization of the *statement* of the result to be proved, that allows the claim to be proven on a technicality. (This is a particular risk if this statement formalization is also AI-generated.)

See https://leanprover-community.github.io/did_you_prove_it.html and https://lean-lang.org/doc/reference/latest/ValidatingProofs/#validating-proofs for best practices on guarding against such issues.