>[!abstract] >**Truth mining** is a metaphor coined by Greg Egan in his novel *Diaspora* which refers to doing mathematics as a form of exploration rather than invention. "Truth mines" are an immersive computational landscape in which mathematical truths already exist as a vast interconnected structure waiting to be discovered. Citizens of the polis literally navigate this landscape, uncovering theorems, examining proofs, and finding new connections between mathematical objects. >[!note] >I am partial to the Platonist idea that mathematics are discovered, not invented (see [[Mathematics]]). The advent of generative AI and formal proof languages such as Lean point in the direction that computer-assisted discovery of new math will become the norm. In that sense, the concept of truth mining is prescient. With analogy to proof of work in blockchains, discovery in math will increasingly become a function of how much CPU or GPU work is expended, i.e., how many tokens are burned. >[!related] >- **North** (upstream): — >- **West** (similar): — >- **East** (different): — >- **South** (downstream): —