Learning Lean
Written by Shahroch Malik Hassany Introduction My task in this project was to understand how a new implementation of the real numbers in Lean works: the ComputableReal Repository. I was supposed to figure out what it does, how it works,…