While I agree with that, my layman's understanding is that the whole purpose of Lean is that once you agree that the program does "do what it says it does", all the intermediate steps can be verified with a compilation.
That is, verifying a proof in English was a painstaking, years long process in the past as independent mathematicians looked for holes in the steps connecting the logic. When the proof is written in Lean, all of that work goes away. My point is that if OpenAI publishes the Lean code (not sure if they already did), verification should take weeks not years.
That is, verifying a proof in English was a painstaking, years long process in the past as independent mathematicians looked for holes in the steps connecting the logic. When the proof is written in Lean, all of that work goes away. My point is that if OpenAI publishes the Lean code (not sure if they already did), verification should take weeks not years.