Comment by oersted

Serious theorem-proving AIs always write the proof in a formal syntax where it is possible to check that the proof is correct without issue. The most popular such formal language is Lean, but there are many others. It's just like having a coding AI, it may write some function and you check if it compiles. If the AI writes a program/proof in Lean, it will only compile if the proof is correct. Checking the correctness of proofs is a much easier problem than coming up with the proof in the first place.