Thread by @getjonwithit

Like @davidbessis and others, I think that Hinton is wrong. To explain why, let me tell you a brief story.

About a decade ago, in 2017, I developed an automated theorem-proving framework that was ultimately integrated into Mathematica (see: youtube.com/watch?v=mMaid2…) (1/15) x.com/vitrupo/status…

The real reason for building it, beyond it just being a fun algorithmic puzzle, was because my then-collaborator @stephen_wolfram and I wanted to perform an empirical investigation: to systematically enumerate possible axiom systems, and see what theorems were true. (2/15)

@stephen_wolfram We constructed an enumeration scheme, set the theorem-prover running, and waited. Unsurprisingly, most axiom systems we encountered were completely barren. But occasionally we'd see one we recognized: group theory shows up around no. 30,000, Boolean logic at ~50,000, etc. (3/15)

@stephen_wolfram Continuing further, we found topology at ~200,000, set theory at ~800,000, and so on. Within each of these systems, the prover quickly rediscovered the standard lemmas and theorems (as well as many more true results that were not immediately recognizable as interesting). (4/15)

@stephen_wolfram Moreover, in between the barren wastelands and the known fields of mathematics, there seemed to be thousands of other "alien" axiom systems: mathematical systems just as rich as topology or set theory, with just as many non-trivial theorems, but which did not correspond... (5/15)

@stephen_wolfram ...to any known mathematical objects or theories that humans had ever investigated. Weird algebraic structures, funky nonstandard logics, operator theories with strange arities, etc. I spent months trying to understand these "alien mathematicses", as well as the... (6/15)

@stephen_wolfram ...new "alien theorems" we'd discovered within existing fields. I developed increasingly sophisticated methods of analysis: one of my favorites was to construct proof graphs, then use vertex outdegrees to assess which lemmas were the "load-bearing" parts of the proof... (7/15)

@stephen_wolfram ...and use those to construct "conceptual waypoints" from which the other parts of the proof could be recursively constructed. But after ~6 months, I gave up. I could learn to manipulate the rules of these systems, I could develop "formal intuitions" for their behavior... (8/15)

@stephen_wolfram ...yet in the end they didn't "make sense" to me on any deep instinctive level. I couldn't figure out why we *cared* about these structures, or what the *stories* behind the theorems were. There was no motivation, no intuition, no big questions to which these were answers. (9/15)

@stephen_wolfram What it made me realize is that mathematics is a fundamentally *human* story. The Babylonians developed arithmetic for commerce. They developed geometry to survey land. We generalized arithmetic to get equations, then abstract algebra. We generalized geometry to get... (10/15)

@stephen_wolfram ...topology, then higher category theory. In the 17th century, the needs of physics and celestial mechanics injected the ideas of calculus, which we generalized to real and complex analysis. We mixed algebra and analysis to get functional analysis and operator theory. (11/15)

@stephen_wolfram We mixed analysis and geometry to get differential geometry, and mixed that with algebra to get tensor calculus, etc. Behind every field and result, there is a deeply human lineage you can trace, stemming from the practical needs and intellectual curiosity of our species. (12/15)

@stephen_wolfram What my adventures in automated theorem-proving (both then and now) have repeatedly taught me is that, in the absence of any human cultural story, these alien mathematicses appear dry, sterile, and desolate, even when they're really brimming with nontrivial theorems. (13/15)

@stephen_wolfram We can automate the proving of theorems, or the discovery of conjectures, or even the invention of new axiom systems, but we can't automate *mathematics*. Because "mathematics" is the name we give to the *human* cultural story, not to the formal methods themselves. (14/15)

@stephen_wolfram So I think Hinton is wrong: formal methods are a closed system, but mathematics is not, and the latter will cease to be mathematics (in any recognizable sense) if allowed to develop independently of human culture for any extended period: it's ultimately about the story. (15/15)