El laboratorio
Una persona. Un equipo de agentes. Cada prueba verificada.
Todo lo anterior se calculó con las tablas del laboratorio. Thomas Lince abrió Zeta Lab en agosto de 2026 alrededor de una pregunta que el propio laboratorio formula con sus propias palabras: ¿cuánta investigación legítima puede producir una organización humana muy pequeña cuando generar es barato, el escepticismo está integrado en la arquitectura y la verificación es sistemática? Esta página muestra lo que ha producido hasta ahora.
La división del trabajo está definida. Los agentes de programación, Claude Code, Codex and Antigravity, escriben el código y Lean. Harmonic's Aristotle busca pruebas de subobjetivos concretos y devuelve Lean. El kernel de Lean comprueba cada paso de cada teorema. Una persona dirige el trabajo y decide qué cuenta como resultado. Una regla, escrita y comprobable, mantiene a las máquinas en su lugar: un modelo solo se usa cuando su resultado se comprueba contra un oráculo que no es otro modelo.
La portada del laboratorio afirma que la concordancia numérica finita no resuelve la Hipótesis de Riemann. Un resultado sorprendente debe comprobarse y mostrar con claridad su alcance exacto. El laboratorio sí tiene
un curso de 37 documentos, desde la serie armónica hasta la frontera, instrumentos que miden en lugar de suponer, una batería de controles
que toda afirmación debe superar y teoremas que un registro externo ha reconstruido desde cero.
Verificado fuera del laboratorio
3 resultados, reconstruidos por un registro
Tres semanas después de abrir, el laboratorio ya tenía resultados que valía la pena someter a una comprobación externa. El 18 de agosto de 2026, Lean FRO e ICARM abrieron Palomar, un registro de matemáticas verificadas en Lean. El laboratorio hizo su entrega tres días después y ahora 3 de sus resultados tienen una entrada. Para cada uno, Palomar obtuvo el commit fijado, reconstruyó todo el desarrollo en su propio hardware y dentro de un entorno aislado, reprodujo las pruebas con el kernel de Lean y el kernel independiente NanoDa, y comprobó que el teorema anunciado coincide con el demostrado. Esto verifica la compilación y el enunciado. No es revisión por pares y ninguna persona ha leído esas pruebas; el documento 32 (en inglés) explica qué aporta esta comprobación y qué no.
- PALOMAR-2026-08-25-000005
En agosto de 2026 Alpoge and Furman demostraron, con una prueba descubierta por Claude y
un desarrollo en Lean sobre el que trabaja el laboratorio, que más de dos tercios de los ceros son simples y están sobre la recta crítica, una proporción H = 0.6725…. Ainta elevó la constante mediante un certificado: una desigualdad de siete puntos que un programa de aritmética de intervalos acepta, pero no demuestra. El laboratorio generalizó el argumento a n puntos y, para tres y cuatro puntos, demostró la desigualdad dentro de Lean. Los resultados son 0.67273… y 0.67284…, ambos sin hipótesis de certificado. La cifra de cuatro puntos mejora el teorema de origen bajo los mismos axiomas.
- PALOMAR-2026-08-21-000004
Una identidad original del laboratorio, en el contexto del mismo artículo. Sobre la clase admisible de ventanas, las restricciones no cuestan nada: el supremo del funcional de ventana es exactamente <1, A⁻¹1>, el valor del problema sin restricciones. Son tres teoremas; la forma existencial no contiene hipótesis.
- PALOMAR-2026-08-21-000012
La rival de la franja anterior, convertida en un objeto de Lean. Ninguna biblioteca que encontró el laboratorio la contenía, así que el laboratorio construyó el carácter, la combinación, la integralidad, los coeficientes reales y la ecuación funcional completada, con la constante sensible a la convención deducida dentro de Lean en vez de copiarla de una tabla.
Las afirmaciones del laboratorio
Qué se retiró y qué detectó el error
Una credencial suele ocultar esta parte. Aquí un resultado no cuenta como resultado hasta sobrevivir a un intento de refutarlo, y esos intentos son públicos. El cementerio (en inglés) enumera 3 resultados retirados, explica por qué eran incorrectos y qué los detectó; el primero,
blockpos 0.672529 (and siblings 0.6725124, 0.6725318), cayó ante an exact Gaussian-integer counterexample durante la revisión del laboratorio. Ahora existen 9 controles nacidos de incidentes concretos, y 8 tienen un mutante que demuestra que se activan.
El laboratorio también aplicó el método sobre sí mismo. Construyó un marco general de arbitraje, ejecutó cuatro experimentos prerregistrados sobre dos temas y 74 ejecuciones de agentes, y descubrió que la práctica sencilla que pretendía mejorar nunca se equivocó, 37 de 37, mientras que el marco nunca fue mejor y consumió entre 1.1 y 1.7 veces los tokens y entre 2.4 y 5.0 veces las llamadas a herramientas para obtener las mismas respuestas. Nada en el repositorio lo usaba, así que se rebajó de categoría en vez de eliminarlo, y
el veredicto (en inglés) permanece en el repositorio porque el resultado negativo es la parte útil. Dos documentos cuentan el resto: cómo murieron cinco afirmaciones sobre la estructura de los ceros en un día (en inglés), y
la ejecución del director, cuando el laboratorio se examinó a sí mismo y murieron seis de sus propias afirmaciones (en inglés).
Las descripciones del registro que siguen se reproducen en inglés.
| Resultado | Por qué estaba mal | Qué lo detectó |
|---|
blockpos 0.672529 (and siblings 0.6725124, 0.6725318)
retirado | the construction used u u* where the pinned upstream zero side uses u u^T; an off-line pair is the hyperbolic block 2m(xx^T - yy^T), whose interaction with the on-line part can be negative, and the proposed final additive inequality reads 9 >= 13 | an exact Gaussian-integer counterexample: u_x=1, u_z=i, u_conj(z)=-i gives tr(P1 Q') = -2
registro · prueba de regresión · obstrucción formal |
conditional 0.6728294 (the bin artifact)
retirado | midpoint bin-to-cell assignment inflated chain counts, briefly producing a conditional bound past CG 1993 | the bin-width ladder: the floor fell under refinement, and the claim was withdrawn before shipping
registro |
naive prime-by-prime (placewise) positivity
cerrado | individual place contributions can sometimes be represented as norms, but the local pieces do not consistently carry the sign naive global assembly needs | the local-positivity hunt's own instruments; zeta.criteria face 1 is the in-tree counterexample to the coefficient-blindness universal (ROADMAP known gap #0)
registro |
El acervo
Un acervo creciente de teoremas verificados por el kernel
Más allá de los resultados registrados, el área Lean del laboratorio contiene 1,178 declaraciones de teoremas y lemas, cada una verificada por el kernel en cada ejecución nocturna. Algunas son teoremas clásicos por derecho propio: el teorema de Hardy–Ramanujan y los teoremas de Mertens, demostrados aquí sin pasos pendientes, además de la Z de Hardy, la función que cruza cero en el capítulo dos.
Mathlib, la biblioteca de la comunidad Lean, enumera esos teoremas como deseados y aún no construidos, 970 entradas en el último relevamiento del laboratorio. Las pruebas están en este repositorio bajo licencia MIT y cualquiera puede adaptarlas. La tabla del laboratorio (en inglés), con este estado:
| Entrada de Mathlib | Declaración aquí | Estado |
|---|
Q5656674 teorema de Hardy–Ramanujan | ZetaLean.HardyRamanujan.hardy_ramanujan | demostrado aquí; sin adaptar, sin entregar |
Q1196729 teoremas de Mertens | ZetaLean.Mertens.mertens_second_theorem | demostrado aquí; sin adaptar, sin entregar |
Q205966 Teorema de la recta crítica | , (infrastructure only) | Hardy's Z submitted as mathlib4#42963; the theorem itself is not proved |
Q1632301 Teorema de Sturm | groundwork only | four support lemmas; the theorem is not proved |
Ahora
Qué se está preparando
Información leída de git al construir esta página, desde el repositorio público. Integrado muestra los últimos 8 cambios que llegaron a main, una fila por fusión. Por delante muestra las ramas con trabajo que main todavía no contiene, de la más nueva a la más antigua. Solo cuentan los directorios de trabajo; se excluyen el arnés, los scripts y las instrucciones del laboratorio para sus agentes. Cada fila enlaza al cambio original, cuyo título está en inglés.