Harmonic presentó públicamente Aristotle Agent, un agente especializado en matemáticas formales. Se trata de una herramienta diseñada para recibir problemas en lenguaje natural, trabajar sobre ellos durante periodos prolongados, producir archivos de proyecto y, en ciertos casos, traducir razonamientos a Lean, un entorno usado para verificar demostraciones con precisión lógica. Harmonic lo ofrece hoy por web, CLI y API, y lo presenta como un sistema capaz de trabajar de forma prolongada sin intervención humana sobre tareas de formalización.
Harmonic ya había mostrado versiones previas del sistema desde 2025, primero en beta y después en reportes técnicos sobre theorem proving de alto nivel. Lo que parece haber ocurrido en marzo de 2026 no es el nacimiento del modelo, sino su empaquetado más abierto como Agent, es decir, como producto con una capa operativa más visible. En otras palabras, la novedad no es solo el “cerebro” matemático, sino la forma en que ese cerebro se convierte en herramienta de trabajo.
Para esta nota, realizamos una prueba diseñada y evaluada con apoyo de GPT-5.4 Thinking, usado aquí como sistema de contraste para formular las preguntas, revisar la corrección conceptual de las respuestas y valorar la plausibilidad de las formalizaciones entregadas. La elección del modelo se realizó a partir de los resultados en ProofBench, benchmark de Vals centrado en matemáticas formales verificables, donde Aristotle aparece con 71% de precisión, mientras GPT-5.4 figura como el foundation model más cercano con 56%.
La primera prueba partió de una intuición tomada del análisis de grafos: si una arista tiene alto solapamiento de vecindad, ¿es poco probable que sea un puente?
I work on graph-based investigative and semantic analysis systems.
Please study the following question in a mathematically rigorous way:
Given a finite undirected graph G = (V,E), define the local neighborhood overlap score of an edge (u,v) as
O(u,v) = |N(u) ∩ N(v)| / |N(u) ∪ N(v) \ {u,v}|
where N(x) is the neighbor set of x.
I want to know whether the following claim is true, false, or only conditionally true:
«If an edge has high neighborhood overlap, then it is unlikely to be a bridge.»
Tasks:
1. State the claim precisely.
2. Determine whether it is always true, false, or true under additional assumptions.
3. Give a proof or a counterexample.
4. If possible, formalize the result in Lean 4.
5. Then explain in plain English how this could matter for identifying structurally fragile links in real-world graphs.
Aristotle reformuló su respuesta como una proposición exacta. Si una arista tiene overlap positivo, entonces no puede ser bridge; dicho al revés, todo bridge tiene overlap cero.
La pregunta original estaba formulada en lenguaje probabilístico, casi heurístico: “high overlap” e “unlikely”. Aristotle limpió esa ambigüedad y la transformó en un enunciado demostrable. La prueba que dio es corta y correcta: si los nodos uu y vv comparten un vecino ww, entonces aunque se elimine la arista (u,v)(u,v) todavía existe el camino alternativo u−w−vu-w-v, por lo que la arista no era un puente.
La importancia de esa primera prueba no fue la profundidad del resultado, sino el tipo de operación intelectual que mostró. Un sistema superficial habría respondido con una frase tipo “si hay caminos alternativos, la conexión parece más estable”. Aristotle hizo algo más sobrio: recortó el lenguaje hasta volverlo demostrable y lo bajó a un archivo de Lean 4. Según el resumen del proyecto, la formalización fue completada sin sorry, es decir, sin dejar huecos abiertos intencionalmente, y el paquete entregado incluyó el análisis y el archivo .lean correspondiente.
La segunda prueba fue más ambiciosa y, por eso mismo, más reveladora. En lugar de pedir una proposición cerrada, se le planteó una distinción muy cercana al problema del pseudoanálisis de redes sociales comunmente realizado por personas que no tienen conocimiento en teoría de grafos y fue previamente analizado por EstadoRed: cómo separar a un hub cohesivo de un broker que parece central solo porque conecta regiones débilmente relacionadas. Aquí Aristotle ya no solo respondió una afirmación puntual, sino que propuso un pequeño marco conceptual. Su criterio central fue mirar la conectividad del subgrafo inducido por la vecindad de un nodo G[N(v)]G[N(v)]: si la vecindad forma un bloque conectado, el nodo se parece más a un hub interno; si se fragmenta en varios grupos, se aproxima más a un broker.
Aristotle explicó por qué el clustering coefficient puede ser engañoso para este tipo de diagnóstico: mide densidad entre vecinos, no necesariamente conectividad. Una vecindad puede tener algunos triángulos y aun así estar partida en dos bloques; del mismo modo, puede ser bastante rala y permanecer conectada. A partir de ahí formuló un resultado más fuerte: si G[N(v)]G[N(v)] es conectado, entonces vv no es un cut vertex; por contraposición, todo cut vertex tiene vecindad desconectada.
En conclusión, aunque tanto el hub cohesivo como el nodo broker pueden presentar un alto grado de conectividad dentro de una red, Aristotle distinguió entre ambos a partir de la estructura de sus vecindades. Mientras un hub cohesivo mantiene a sus vecinos vinculados entre sí, un broker conecta grupos que pueden estar débilmente relacionados o incluso separados sin su mediación. A través de un resultado formal, mostró que si la vecindad de un nodo forma un subgrafo conectado, su eliminación no fragmenta la red del mismo modo que sí puede ocurrir con un punto de articulación. Esta diferencia estructural es relevante para el análisis de redes sociales, porque permite distinguir entre nodos que concentran cohesión comunitaria y nodos que funcionan como intermediarios entre comunidades distintas.
También es pertinente destacar que los términos utilizados por Aristotle, tales como Hub Cohesivo y broker no son comunmente utilizados en la literatura sobre teoría de grafos. No parecen alucinaciones en el sentido fuerte, sino categorías analíticas ad hoc construidas por el modelo a partir de conceptos reales de grafos. La parte matemática seria de su respuesta no dependió tanto de los nombres raros, sino del resultado estructural: la relación entre la conectividad de G[N(v)]G[N(v)] y que vv sea o no un cut vertex.
La experiencia de uso también dejó un matiz importante sobre la palabra agentic. Aunque Harmonic presenta a Aristotle como agente matemático, en esta prueba esa dimensión no fue explorada a fondo. No se le pidió editar grandes repositorios, abrir pull requests complejas ni ejecutar cadenas largas de herramientas. Aun así, la experiencia sí se sintió distinta a la de un chatbot convencional: el sistema tomó tiempo prolongado para procesar la consulta, generó varios archivos de trabajo y finalmente entregó el resultado por correo electrónico. La capa agentic apareció, sobre todo, como modalidad operativa: menos respuesta instantánea en una caja de texto, más ejecución prolongada que devuelve un pequeño paquete de proyecto. Eso coincide con la forma en que Harmonic lo describe públicamente, como sistema capaz de trabajar dentro de proyectos Lean o repositorios.
En herramientas como Aristotle, el principal problema no parece estar en una autonomía desbocada de ciencia ficción, sino en el tipo de entornos donde probablemente será adoptado: repositorios privados, pruebas formales en desarrollo, código experimental y líneas de investigación todavía no publicadas. Harmonic presenta a Aristotle como un sistema capaz de trabajar dentro de proyectos y repositorios, pero al mismo tiempo sus términos aclaran que no garantizan exactitud, integridad ni adecuación para usos particulares, y que el servicio no está diseñado para procesar información personal. En ese contexto, el riesgo no es que el agente “quiera” hacer algo indebido, sino que pueda modificar archivos sensibles, introducir errores difíciles de detectar o trasladar conocimiento técnico delicado a una infraestructura externa sin que el usuario tenga pleno control de cada paso.
En campos como verificación formal, criptografía o blockchain, donde un cambio pequeño puede tener efectos desproporcionados, la potencia del agente no elimina la necesidad de supervisión; al contrario, la vuelve más importante. La promesa de un agente matemático también convierte a la propia investigación en su principal superficie de riesgo. Cuanto más útil resulta para trabajar sobre pruebas y proyectos reales, más cerca queda de intervenir en conocimiento técnico todavía frágil, privado o en proceso.
