Comment by ghm2180

I think the only way MS knows how to make money is lock someone into an ecosystem. I think their next attempt should be a closed source lean checker that has will have proprietary code for NL -> lean formalization checker.