5 ms·

Regarding automatic formalization of proofs using AI, how do we know the formalization doesn't contain errors?

• Jblx2 6d ago
  In a similar vein, where does the theorem statement even reside, just so we can take a look at how large that is? Is it the four files with "Theorem" (and no "Comparator") in the file name? ("R3/Theorem.lean", "LocalPaperTheorem.lean", "PeriodiocPaperTheorem.lean", and "WholeDomainPhysicalStageTheorem.lean"). https://github.com/openai/NavierStokesAndEuler/blob/main/NavierStokes/R3/Theorem.lean https://github.com/openai/NavierStokesAndEuler/blob/main/Nav... ?
• Ohentis 6d ago
  It depends on what you mean by that. In general we hope that the environment and theorum statements are correct. If they are, we know that the formal proof proves the theorum we want. If your asking how we know that the formal proof actually matches the informal proof, we do not.