Aproximadamente Theorem.chat
Theorem.chat toma unha afirmación matemática e tenta resolvela. Vostede indicafirmación e o estándar que ten que cumprir. Un panel de modelos de IA - tantos como queira, de calquera vendedor que queira - atacafirmación e un modelo máis arbitra. Logo o argumento formalízase en Lean 4 contra Mathlib, e o núcleo Lean decide se se proba. O último paso é o produto.
Por que un núcleo, e non outro modelo
Faga unha pregunta difícil a un modelo e obterá unha resposta fluída se é correcta ou non. Pregunte a varios e a miúdo concordan, o que se sente como unha confirmación e non o é: os modelos comparten datos de adestramento e puntos cegos. Un segundo modelo que comprobe o primeiro é aínda o mesmo tipo de xuízo, e pode ser discutido. O núcleo Lean non pode. Ou derivafirmación dos axiomas e Mathlib, ou non o fai, e a confianza non ten efecto no resultado.
Compróbanse e rexéitanse as formas habituais de falsificar unha proba formal. Unha proba que deixe un burato con sorry, unha que apele a native_decide para facer que o núcleo faga un cálculo de confianza, ou unha que introduza silenciosamente un axioma novo, é detectada e rexeitada en vez de contarse como un éxito.
O que pode facer realmente o panel
A argumentación é a parte barata. O panel traballa coa literatura - arXiv, OpenAlex, Crossref - polo que un resultado coñecido é citado en vez de ser mal derivado. Ten SageMath e PARI/GP para computación, Z3 e CVC5 para resolver SMT, OEIS para procurar e identificar unha secuencia que construíu, e un ambiente Python en sandbox sen acceso á rede. Unha conxectura pode ser probada contra dez mil casos antes de que alguén pase unha rolda tentando probala, e un contraexemplo remata a discusión inmediatamente.
Evidencia, non elocuencia
Unha coincidencia non se puntua pola calidade dos argumentos. A afirmación descompóñense en criterios de aceptación, e un criterio só se resolve cando algo detrás del pode ser comprobado por un terceiro: unha fonte coa pasaxe relevante citada, ou código que foi realmente executado coa súa saída real. O árbitro comproba esa evidencia antes de decidir, e non pode declarar que a coincidencia rematou mentres un criterio aínda está aberto.
Ti estableces o estándar
O estándar é o que vostede escolle, e o árbitro manténdoo literalmente. Pídalle o que un experto coidadoso aceptaría e obterá iso. Pídalle un argumento dedutivo completo con todas as suposicións e será xulgado contra iso. Pídalle o nivel que un premio envía e o resultado honesto é normalmente unha conta precisa de onde o panel fallou - que vale máis que unha afirmación segura que tería que comprobar vostede mesmo de calquera xeito.
Para ser claro: esta non é unha máquina que resolve problemas abertos. É unha máquina que rexeita deixar pasar un argumento como resolto cando non o é, e que lle di exactamente que paso fallou.
Unha formalización fallada é a saída útil
Cando Lean non pecha a proba, obtén o obxectivo exacto que queda. Na práctica ese é case sempre o punto onde o argumento informal estabacenar coa man - o paso que todos os que leron a versión en prosa terían asinado. Entón ese obxectivo é entregado a calquera asento que estea mellor situado para atacar, xunto co que xa se tentou, e nada máis. Os modelos caen cando están atascados, reexprimíndose a si mesmos a custo total; pasar unha pregunta específica no canto normalmente desbloquea por unha fracción das fichas.
O traballo longo sobrevive
Cada lema que o panel estabelece vai para un libro compartido coa súa proba, polo que os resultados escríbense unha vez e nunca se derivan de novo, e os puntos mortos rexistranse para que ninguén volva a eles. As coincidencias executanse no lado do servidor e pausanse limpas - no orzamento, por un fallo do provedor ou porque pechou a páxina - e reanúdanse exactamente onde se pararon.
Para que non é isto
Teorema é unha palabra dedutiva. Este sitio está feito para matemáticas, lóxica, informática teórica, física teórica e teoría económica - campos nos que unha afirmación é resolta por proba. As preguntas empíricas en bioloxía, medicina, química ou ciencias sociais non producen teoremas, producen descubrimentos, e ningunha cantidade de formalización as decidirá. O noso sitio irmán referee.chat executa o mesmo proceso de panel e revisor sen o paso Lean, para exactamente esas preguntas.