| ▲ | davesque 4 hours ago | |
Regarding automatic formalization of proofs using AI, how do we know the formalization doesn't contain errors? | ||
| ▲ | Jblx2 31 minutes ago | parent [-] | |
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/Nav... ? | ||