Hacker News Reader

> 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?

View on HN

You 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.

It'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.

Reply on news.ycombinator.com