Kevin Buzzard wanted to use Lean to formalize papers in his field, establish with complete certainty whether they were correct, repair incorrect papers, and regain confidence to continue research when the formalized results checked out.

“So to him, that was the draw of Lean, was he wanted to take these papers that had developed in his field, formalize them, like convert them into this computer programming language, determine with complete certainty whether, whether they were correct, and if they weren't, fix them, but if they were, then it would just kind of give him, uh, renewed confidence to kind of proceed in research in this area.”