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.
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.