3 ms·
That is the point. Someone must verify that the Lean matches the actual theorem, precisely as it should be interpreted.
by nicce 25d ago
That is the point. Someone must verify that the Lean matches the actual theorem, precisely as it should be interpreted.
- latent-person 25d agoWhich has nothing to do with the total number of lines, it's just the theorem statement you need to check. Here is what they showed, which is under 300 lines with comments https://github.com/openai/NavierStokesAndEuler/blob/main/ComparatorChallenges/NavierStokes.lean https://github.com/openai/NavierStokesAndEuler/blob/main/Com...
- nicce 25d agoThat seems to be indeed true. I guess it gets validated quite soon.