9 ms·
> However, checking that a given Lean repository actually proves the claimed statement is somewhat non-trivial, especially for an audience which is not expert i
by demibabs 2mo ago
> However, checking that a given Lean repository actually proves the claimed statement is somewhat non-trivial, especially for an audience which is not expert in the use of Lean
Isn’t this kind of a recursive problem where you now have to prove your proof that their proof proves their claimed statement?
- red75prime 2mo agoIt's not a proof. You check that the mathematical ideas expressed in the claimed statement are the same as the mathematical ideas expressed by the Lean repository.
- emil-lp 2mo agoYou only have to prove the formalization of the theorem statement. The formalized statement is guaranteed to be true if Lean says so. There will always be a leap from the real world to the formal world.