Mochizuki mentions Lean-style computer formalization as the "best hope" for "bridging the gap between the social/political dynamics surrounding social acceptance of mathematical (or, more generally, scientific) ideas and mathematical truth," while noting it won’t persuade those insisting the circle is a square, formally or otherwise ("faith en masse").
He writes:
>In this context, I am reminded of the (perhaps humorously anachronistic) phenomenon of “flat-earthers”, as well as the following stories that I heard when I was a graduate student in the late 1980’s to early 1990’s at Princeton University:
>· some local government in the United States of America passed a law to the effect that, within its local jurisdiction, π (i.e., the length of the cirumference of a circle of unit radius) is equal to 3;
> · some survey of the general population of the United States of America found that a surprising percentage of the population believe that one-third is greater than one-half (i.e., “ 1/3 > 1/2 ”), that is to say, since three is greater than two.
>In either of these two cases, it seems highly unlikely that presenting a Lean-style computer formalization of the irrationality of π or of the inequality 1/2 > 1/3 to the people involved would result in a change in the minds or hearts of these people.