Comment by jrflo
6 hours ago
So my guess is that they have the AI system attempt to prove the theorem in natural language, then try to generate a Lean proof for it, and in that process they end up with a slightly different solution as the autoformalizer is essentially rewriting the NL proof to make it formalizable? Do we just need a "reverse pass" to re-align the NL proof with the Lean code?
Also, it doesn't seem that they are questioning the truthfulness of either proof, just that they are different?
Generating the lean proof first is a viable approach as well followed by an explanatory pass.
Actually, they are questioning whether the natural language description of the proof is either not faithful to the formal proof, or simply wrong, or both.