I worked on formal proof in 2014, but abandoned it when I realized academic mathematicians would never use it. Formal proof would have helped math’s consumers: better search, fewer mistakes, easier translation (to other human languages), etc.. But academic mathematicians didn’t care about math’s users very much.

Now that there are tools that help math’s consumers and because the economy of proof production wasn’t oriented towards consumers, there is a real chance that academic mathematicians get sidelined.