Resumen: Las matemáticas humanas (HM), las matemáticas que los humanos descubren y valoran, son un subconjunto cada vez más pequeño de las matemáticas formales (FM), la totalidad de todas las deducciones válidas. Sostenemos que HM se distingue por su compresibilidad a través de definiciones, lemas y teoremas anidados jerárquicamente. Modelamos esto con monoides. Una deducción matemática es una serie de símbolos primitivos; una definición o teorema es una subcadena o macro con nombre cuyo uso comprime la cadena. En el monoide abeliano libre $A_n$, un conjunto de macros logarítmicamente disperso logra una expansión exponencial de la expresividad. En el monoide libre no abeliano $F_n$, incluso un conjunto de macros polinomialmente denso solo produce una expansión lineal; la expansión superlineal requiere una densidad casi máxima. Probamos estos modelos con MathLib, una gran biblioteca de matemáticas Lean~4 que tomamos como proxy de HM. Cada elemento tiene una profundidad (capas de anidamiento de definiciones), una longitud envuelta (tokens en su definición) y una longitud desenvuelta (símbolos primitivos después de expandir completamente todas las referencias). Encontramos que la longitud sin envolver crece exponencialmente tanto con la profundidad como con la longitud envuelta; La longitud envuelta es aproximadamente constante en todas las profundidades. Estos resultados son consistentes con $A_n$ e inconsistentes con $F_n$, lo que respalda la tesis de que HM ocupa un subconjunto de crecimiento polinomial del espacio FM de crecimiento exponencial. Discutimos cómo la compresión, medida en el gráfico de dependencia de MathLib, y un análisis estilo PageRank de ese gráfico pueden cuantificar el interés matemático y ayudar a dirigir el razonamiento automatizado hacia las regiones comprimibles donde viven las matemáticas humanas.
Publicado originalmente en export.arxiv.org el 23 de marzo de 2026.
Ver fuente original
