“Formal proof” and “mechanized proof” are not synonymous. And proof assistants have a long way to go before they can be useful for mathematics in general.