An AI-translated proof may pass Lean checks despite an error in the original

A post says a new paper shows a chatbot silently correcting a wrong math proof to produce a valid Lean proof. According to the post, passing Lean’s check says nothing about whether the original proof was right. The post also says knowing when a statement can be translated faithfully is provably harder than the Halting problem, so no AI translator can always do it.