Formalized in Lean, just five months ago [0], resulted in discovery of bugs. Just because Lean can compile it, does not mean it is safely proven. It is the sta

Formalized in Lean, just five months ago [0], resulted in discovery of bugs. Just because Lean can compile it, does not mean it is safely proven. It is the start of a process to check whether something actually holds, not the end. [0] https://news.ycombinator.com/item?id=47759709 https://news.ycombinator.com/item?id=47759709