A place for reactions to and questions about siliconreckoner.substack.com.

…beyond my interest in how current trends in mechanization of mathematics force me to sharpen my own understanding of what makes mathematics valuable as a human practice (as in this close reading of a magnificent lecture by Dick Gross), I am deeply interested in mechanization of mathematics, of which formalization is a small part, as a social phenomenon: how it establishes a shared vocabulary, an ideology, a system of values, a community; how it overlaps with and is influenced by broader economic and industrial trends; what it does or does not share with contemporary political movements; and much more. In this respect the leanprover-community Zulip Chat Archive is a veritable socio-historical goldmine. And with that in mind I encourage you to direct your comments to this page.