In 2015, Leonardo de Moura submitted a paper about his proof assistant, Lean. It was rejected.
The reviewer asked, "Why do we need another proof assistant?"
At Microsoft, Leo and Nikolaj Bjorner had spent years developing Z3, a tool designed to catch software bugs.
But when engineers tried using it to prove their code was correct, it produced unstable results.
One engineer vented: "Come on, man, I just want to convince the system that my proof is correct."
So Leo started building something better.
He called it Lean because Z3 had grown bloated, and he wanted the code to be clean.