Throughout the twentieth century, mathematical researchers repeatedly returned to a powerful dream: that formalization and automation might overcome fragmentation by producing a universal language of proof. This lecture revisits that dream through the history of automated theorem proving and the QED Project, treating automation not merely as a technical innovation but as a theory of social and epistemic organization. Efforts to mechanize proof embedded assumptions about trust, resources, authority, labor, and coordination—about who or what should be relied upon to know when something is true. This talk explores how the dream of universalism, consolidation, and automation functions as a response to social and institutional pressures rather than purely epistemic ones. The efforts to bring all of mathematics under one formal order and automate it was never and has never yet been achieved – but attempts to do so offer compelling windows into the relationship between mathematical practice, mathematical ideals, and mathematical contestations.