Alrededor de Theorem.chat
Theorem.chat toma una reclamación matemática y trata de resolverla. Usted declara la reclamación, y el estándar que tiene que cumplir. Un panel de modelos de IA — tantas como desee, de los proveedores que desee — lo ataca, y un árbitro modelo más. Entonces el argumento se formaliza en Lean 4 contra Mathlib, y el núcleo Lean decide si se prueba. Ese último paso es el producto.
¿Por qué un núcleo, y no otro modelo
Haga un modelo una pregunta difícil y usted consigue una respuesta fluida si es correcto o no. Pregunte varios y a menudo están de acuerdo, que se siente como corroboración y no es: los modelos comparten datos de entrenamiento y comparten puntos ciegos. Un segundo modelo comprobando el primero sigue siendo el mismo tipo de juicio, y se puede hablar de ello. El núcleo Lean no puede. O bien deriva la declaración de los axiomas y Mathlib, o no, y la confianza no tiene efecto en el resultado.
Las formas habituales de falsificar una prueba formal son revisadas y rechazadas. Una prueba que deja un agujero con sorry, una que apela a native_decide para hacer que el núcleo tome un cálculo en confianza, o una que introduce silenciosamente un nuevo axioma, es detectada y rechazada en lugar de contar como un éxito.
Lo que el panel puede hacer realmente
El panel trabaja con la literatura —arXiv, OpenAlex, Crossref— por lo que se cita un resultado conocido en lugar de re-derivarse mal. Cuenta con SageMath y PARI/GP para computación, Z3 y CVC5 para resolución de SMT, OEIS búsqueda para identificar una secuencia que ha construido, y un entorno Python arenoso sin acceso a red. Una conjetura puede ser probada contra diez mil casos antes de que alguien pase una ronda tratando de probarlo, y un contraejemplo termina la discusión inmediatamente.
Pruebas, no elocuencia
Una coincidencia no se marca en calidad de argumento. La reclamación se descompone en criterios de aceptación, y un criterio sólo se resuelve cuando algo detrás de ella puede ser re-chequeado por un tercero: una fuente con el pasaje pertinente citado, o código que fue ejecutado realmente con su salida real. El árbitro vuelve a comprobar que la evidencia se encuentra antes de la sentencia, y no puede declarar que la coincidencia terminó mientras un criterio está todavía abierto.
Tú pusiste la barra
El estándar es tuyo para elegir, y el árbitro lo sostiene literalmente. Pregunta por lo que un experto cuidadoso aceptaría y usted consigue eso. Pide un argumento deductivo completo con cada suposición declarada y usted consigue juzgado en contra de eso en su lugar. Pide la barra una presentación de premio se enfrentaría, y el resultado honesto es generalmente una cuenta precisa de donde el panel se quedó corto - que vale más que una afirmación segura que tendría que comprobar a sí mismo de todos modos.
Para ser claros sobre ello: esta no es una máquina que resuelve problemas abiertos. Es una máquina que se niega a dejar pasar un argumento como resuelto cuando no lo es, y que le dice exactamente qué paso falló.
Una formalización fallida es la salida útil
Cuando Lean no cierra la prueba, obtienes el objetivo exacto que queda. En la práctica, ese es casi siempre el punto donde el argumento informal fue la agitación de manos — el paso que todo el mundo leyendo la versión de prosa habría asintió pasado. Ese objetivo se entrega entonces a cualquier asiento que esté mejor situado para atacarlo, junto con lo que ya se ha intentado, y nada más. Modelos thrash cuando están atascados, repitiéndose a todo costo; pasando una pregunta específica en lugar de desbloquear generalmente para una fracción de las fichas.
Sobrevive un largo trabajo
Cada lema que establece el panel entra en un libro mayor compartido con su prueba, por lo que los resultados se escriben una vez y nunca se vuelven a derivar, y se registran los callejones sin salida para que nadie vuelva a entrar en ellos. Los partidos corren al lado del servidor y se detienen limpiamente —en el presupuesto, en un corte del proveedor o porque cerraste la pestaña— y reanudan exactamente donde se detuvieron.
Para lo que no es esto
El teorema es una palabra deductiva. Este sitio está construido para matemáticas, lógica, informática teórica, física teórica y teoría económica — campos donde una reclamación se resuelve por la prueba. Cuestiones empíricas en biología, medicina, química o las ciencias sociales no producen teoremas, producen hallazgos, y ninguna cantidad de formalización los decidirá. Nuestro sitio hermana referee.chat ejecuta el mismo proceso de panel y consulta sin el paso Lean, para exactamente esas preguntas.
referee.chat — la misma idea, para las afirmaciones empíricas