> This mirrors the Lean statement and Lean proof situation. The statement is like an interface, and the proof is like the implementation behind that interface.

> This mirrors the Lean statement and Lean proof situation. The statement is like an interface, and the proof is like the implementation behind that interface. This is true in a very deep sense due to the Curry-Howard correspondence and calculus of constructions which are central to Lean. In Lean, the proposition you are proving is a type (so it really is an interface directly in the computer science sense) and the proof is a function which takes your hypotheses and returns a term of that type (so it really is the implementation of that interface). In fact in lean, you can just as well write this implementation as a lambda (this is known as “term mode”) as in the “tactic mode” that is more generally used in normal lean use. Lean really doesn’t care at all which one you use and you can switch between them within a proof quite easily without interfering with lean’s ability to check your proof at all. > Which really makes me wonder about the actual value proposition of Lean then, but alas... The purpose of lean really is quite different from what most people on hn seem to want it to be. Lean is designed to be a useful tool for mathematicians who want to formalise areas of mathematics. It’s not a primary goal of most of the lean community to make something that is hardened against malicious proof attempts (although these are considered bugs and there is a small subcommunity who work on this area in particular). So it isn’t primarily for the benefit of people who want to “fire and forget” some proof without reading or understanding it and just get the check mark if it’s true.[1] It’s mainly for mathematicians who want a proof assistant to help them with their work. [1] there are sub-tools such as comparator that are designed for this type of use case. https://github.com/leanprover/comparator https://github.com/leanprover/comparator