Neither in grade school nor in research seminars does anyone actually present every detail of a mathematical proof with complete rigor. Our faith in a given theorem is ultimately based on the belief that mathematicians could, if asked, fill in all the missing definitions and arguments rather than on the belief that they have already anticipated and answered every possible question. As proofs have grown more complicated and lengthy, even famous mathematicians sometimes admit that they are not quite sure whether their argument is entirely correct. Shouldn’t computers be able to help? Among open-source software projects designed to assist with formulating and checking mathematical proofs, one has emerged as the clear frontrunner. Launched by Leonardo de Moura when he was working at Microsoft Research in 2013, it is called 'The Lean Proof Assistant.' A Lean user inputs a theorem statement along with the steps of a purported proof in a special language. Based on the definitions, results, and logical rules it already knows, the program tries to check each step mechanically. In some cases, it can suggest shorter arguments. In others, it may interactively request more details. But once verified this way with super-human reliability, the theorem and its proof become part of the resources that Lean can call upon going forward. So far, educational resources based on Lean are helping students learn to construct proofs even when a skilled teacher is unavailable. Publications like Wired, Nature, and Quanta have hailed Lean, the last of these calling the Version 3 release 'one of 2020’s biggest breakthroughs in mathematics.' Even Fields Medalists like Peter Scholze praise Lean, which helped verify an important proof of his that was so long, subtle, and impenetrable that he described it as 'a thick jungle.' Despite all this excitement, Lean is still in its developmental stages with much hard work left to improve automation, scalability, usability, and sustainability. As Sloan found out years ago, usual academic structures and incentives are not well suited for such tasks. This is the motivation for launching a 'Focused Research Organization.' Known as a FRO, this is a new type of nonprofit start-up pioneered by PI Adam Marblestone. Each FRO takes on a specific challenge and works on it exclusively for a few years before disbanding. During this time, the FRO will be incubated at the new nonprofit called Convergent Research founded with core funding and backing from Schmidt Futures. Lean creator Leonardo da Moura will lead the FRO technical team, which, in addition to mathematical experts and software engineers, will also include product, project, and community managers. The sustainability plan calls for spinning out a nonprofit Lean Foundation as has been done successfully by other major open-source software projects supported by Sloan that have turned out to be totally transformational. In this case, Lean stands to accomplish nothing less than accelerating the use, discovery, and learning of mathematical truths.