Type checker may be wrong – Lean and the Curry-Howard correspondence

Contents The Curry-Howard correspondence How do proof assistants use the CH correspondence A theorem A proof of the theorem The type checker Limitations of the type checker Mathematical consequences (and proof) Your type checker maybe wrong Conclusion When writing code many of us have been saved time and time again by type checkers: the useful piece of software that ensures you aren’t adding a string to an integer 1 or returning a reference to a value instead of the owned value. However, while useful, and sometimes annoying, it seems that the humble type checker has limited capability beyond its noble task of saving our asses…