From Chiang’s story: ”But as metahumans began to dominate experimental research, they increasingly made their findings avail- able only via DNT (digital neural transfer), leaving journals to publish second-hand accounts translated into human language. Without DNT, humans could not fully grasp earlier developments nor effectively utilize the new tools needed to conduct research, while metahumans continued to improve DNT and rely on it even more. Journals for human audiences were reduced to vehicles of popularization, and poor ones at that, as even the most brilliant humans found themselves puzzled by translations of the latest findings.”
A quote your post: ”The likely outcome is that formalized mathematics will now develop in two separate layers, an intelligible layer embodied by Mathlib, and an unintelligible layer we might call Mathslop, a library of results that are known to be correct via proofs that no human has ever understood.”
an intelligible layer embodied by Mathlib, and an unintelligible layer we might call Mathslop
That sounds transient too. If there are superhuman AIs around and humans are not dead, then, it would likely be trivial to get them to legibilize those results up to the limits of what humans can take in and/or uplift the humans to slurp it up natively.
Related: Ted Chiang’s The Evolution of Human Science. (N.B. this is work of fiction.)
From Chiang’s story:
”But as metahumans began to dominate experimental research, they increasingly made their findings avail- able only via DNT (digital neural transfer), leaving journals to publish second-hand accounts translated into human language. Without DNT, humans could not fully grasp earlier developments nor effectively utilize the new tools needed to conduct research, while metahumans continued to improve DNT and rely on it even more. Journals for human audiences were reduced to vehicles of popularization, and poor ones at that, as even the most brilliant humans found themselves puzzled by translations of the latest findings.”
A quote your post:
”The likely outcome is that formalized mathematics will now develop in two separate layers, an intelligible layer embodied by Mathlib, and an unintelligible layer we might call Mathslop, a library of results that are known to be correct via proofs that no human has ever understood.”
That sounds transient too. If there are superhuman AIs around and humans are not dead, then, it would likely be trivial to get them to legibilize those results up to the limits of what humans can take in and/or uplift the humans to slurp it up natively.