Following last week's first machine- identified structural flaw in a physics paper, this week Quanta Magazine surfaces the internal debate about whether machine-formalized proofs are rigor or something adjacent to it. The question being avoided: if a proof is formally verified but not humanly understandable, what has been established?
