← Back to context Comment by robotpepi 1 day ago How much lean code do you need to read to check if NAvier-Stokes was correctly formalized? 3 comments robotpepi Reply returningfory2 1 day ago A tiny fraction compared to the proof, I'm guessing.But the point is that you don't need to check the proof. But a lot of people seem to misunderstand what's happening and think you still need to check the Lean proof that AI outputs. j16sdiz 14 hours ago tiny fraction compared to the proof, yes.but the proof is so fk'ing large that, the "tiny fraction" is still quite large.and it is not that clean cut, sometimes you need to read the proof to understand the context. You need the context to know if the assumption is true.
returningfory2 1 day ago A tiny fraction compared to the proof, I'm guessing.But the point is that you don't need to check the proof. But a lot of people seem to misunderstand what's happening and think you still need to check the Lean proof that AI outputs. j16sdiz 14 hours ago tiny fraction compared to the proof, yes.but the proof is so fk'ing large that, the "tiny fraction" is still quite large.and it is not that clean cut, sometimes you need to read the proof to understand the context. You need the context to know if the assumption is true.
j16sdiz 14 hours ago tiny fraction compared to the proof, yes.but the proof is so fk'ing large that, the "tiny fraction" is still quite large.and it is not that clean cut, sometimes you need to read the proof to understand the context. You need the context to know if the assumption is true.
A tiny fraction compared to the proof, I'm guessing.
But the point is that you don't need to check the proof. But a lot of people seem to misunderstand what's happening and think you still need to check the Lean proof that AI outputs.
tiny fraction compared to the proof, yes.
but the proof is so fk'ing large that, the "tiny fraction" is still quite large.
and it is not that clean cut, sometimes you need to read the proof to understand the context. You need the context to know if the assumption is true.