I don't think Mathematicians themselves didn't like this idea. In fact Hilbert tried it (https://en.wikipedia.org/wiki/Hilbert%27s_program https://en.wikipedia.

I don't think Mathematicians themselves didn't like this idea. In fact Hilbert tried it (https://en.wikipedia.org/wiki/Hilbert%27s_program https://en.wikipedia.org/wiki/Hilbert%27s_program) one hundred years ago and it failed and proved to be not possible. Well maybe the Hilbert program is too aggressive, and this Lean thing is much moderate. But at the end of the day, the boundary of what program solver could do is bounded already hence no one is paying too much attention.