Proyectos seleccionados. Hechos para usarse. Creados para explorarse.
Un producto independienteMúsica, teoría y software
♫
Modal Runs
Piensa menos. Toca más.
Una app de guitarra que escucha lo que tocas, muestra dónde estás y te ofrece un mundo musical por explorar. Lo construí entero: desde la teoría y el motor de sonido hasta el producto que los envuelve.
Investigación independiente◉ Investigación y demostraciones públicas
ζ
Zeta Lab
Un laboratorio de investigación con IA. Con un teorema como resultado.
Construí un entorno de investigación donde agentes de IA exploran las matemáticas y núcleos de pruebas verifican los resultados. El trabajo incluye una ampliación del resultado de Anthropic sobre zeta, verificada formalmente.
La altura muestra la magnitud logarítmica muestreada, recortada para su visualización. La curva naranja sigue la columna muestreada más cercana a σ = ½. Explora la función aquí; el resultado demostrado se presenta por separado.
Basado en el trabajo de Furman y Alpöge en Anthropic: 67.25007% a 67.28470%, una ampliación de 0.03463 puntos porcentuales. El avance anterior de 41.6% a 67.25% es suyo.
¿Qué significa esto, en palabras sencillas?
Zeta Lab es donde construyo herramientas para que agentes de IA exploren las matemáticas. Los agentes proponen ideas; el software de verificación de pruebas comprueba los resultados formales. La cifra de arriba es una ampliación verificada de una investigación anterior, con el crédito al trabajo original indicado a su lado. No demuestra la hipótesis de Riemann.
01 / Explorar
Los agentes trabajan en paralelo.
Proponen ideas matemáticas y ponen a prueba los candidatos.
02 / Formalizar
Una afirmación se convierte en una demostración.
El enunciado formal y su demostración se escriben en Lean.
03 / Verificar
Los núcleos de pruebas lo verifican.
Lean y NanoDa reconstruyen el resultado registrado de forma independiente.
Explora la línea críticaUn estudio numérico interactivo +
ζ(½ + it) / Z de HardyCalculado aquí
tceros visiblesencontrados
Cada punto es un cambio de signo de la función Z de Hardy, calculado en tu navegador. Este estudio numérico es independiente de la demostración formal. El resultado registrado es una cota asintótica verificada, no una demostración de la hipótesis de Riemann; la verificación por un núcleo de pruebas es distinta de la revisión por pares.
Herramientas de investigación con IA. Agentes que exploran ideas. Resultados que puedes verificar.
Investigación independiente◉ Objetos de prueba publicados
∀
Redes verificadas en Lean
Redes entrenadas. Verificadas en cada entrada.
Agentes de IA entrenaron un transformer pequeño y demostraron en Lean que suma correctamente para cada par de entrada. Después construyeron una verificación en Lean de un certificado de seguridad para una red ACAS Xu. El resultado del transformer cubre todos los pares de entrada; el de ACAS cubre la caja de entrada especificada para la propiedad 1. Un verificador de pruebas implementado por separado volvió a comprobar el cierre de dependencias exportado de cada teorema.
a, b ∈ 0 … 11212,769 celdas, una por cada par de entrada
X₁, X₂ ∈ [−½, ½]34 hojas, recortadas de la caja de entrada
Cada celda y cada hoja es un caso verificado. Señala una.
El cuadrado de pares: cada celda (a, b) está sombreada según la respuesta que el teorema demuestra que el modelo devuelve, (a + b) mod 113. El plano de hojas: una proyección de las 34 cajas de hojas de cinco dimensiones sobre X₁ y X₂, con 32 rectángulos distintos y dos divisores simbólicos para los cortes en X₀; la caja turquesa es la hoja 38, la de menor margen verificado. Ambos dibujos visualizan los resultados verificados; el núcleo comprobó certificados aritméticos y cobertura, no estas imágenes. Los resultados se reportan al lado.
Transformer entrenado verificado en Lean
12,769
Un transformer entrenado de una capa y cuatro cabezas, con pesos enteros y softmax real exacto, suma módulo 113 correctamente para cada par de entradas.Lean × NanoDaLee la historia de la prueba
Modelo diminuto, tarea de juguete, fuerza bruta sobre todas las entradas: se demuestra el modelo redondeado a enteros, no el checkpoint de punto flotante. Objetos de prueba publicados y verificaciones.
Trabajo previo: el proyecto de Brian Naughton certified-grokking certifica la misma arquitectura con un núcleo de aritmética de intervalos en Python que se toma como confiable; el trabajo en Coq de Jason Gross demuestra la exactitud de transformers entrenados para obtener el máximo de dos números. El modelo y los límites de confianza son distintos.
Certificado de ACAS Xu verificado en Lean
34/34
Las 34 hojas verificadas y la caja de entrada cubierta. Agentes de IA construyeron una verificación en Lean de un certificado de alpha-beta-CROWN para la red ACAS Xu 1_1, propiedad 1, usando TorchLean y el benchmark VNN-COMP.Lean × NanoDaVer la evidencia de ACAS
Semántica real exacta, solo axiomas estándar. El importador ONNX está auditado, pero no se ha demostrado formalmente su corrección. Sin afirmaciones sobre ejecución IEEE ni comportamiento de aeronaves.
¿Qué significa esto, en palabras sencillas?
Dos redes neuronales pequeñas y, para cada una, un teorema que el núcleo de pruebas de Lean aceptó: el transformer da la respuesta correcta para cada una de sus 12,769 entradas posibles, y la red ACAS Xu se mantiene por debajo del umbral indicado en toda la caja de entrada indicada. Agentes de IA escribieron las pruebas; dos verificadores independientes las aceptaron. No dice nada sobre modelos grandes, hardware de punto flotante ni aeronaves.
Redes pequeñas. Rangos de entrada completos. Pruebas que un núcleo aceptó.
La IA contesta la llamada. El software conecta lo que sigue.
Desde 2025, agentes de voz que construí contestan el teléfono de una agencia de limusinas en dos mercados de Estados Unidos. El agente cotiza con la lógica de tarifas vigente, hace la retención en la tarjeta y entrega la reserva a una persona para su revisión. Clientes reales, dinero real, incluidas las tres de la mañana.
En producción, no una demostración. Dirigí esa operación desde 2019 antes de escribir el software que la gestiona.
La IA se encarga de la conversaciónLlamadas y preguntas de clientes
02
El software prepara el siguiente pasoCotizaciones, reservas y estado del pago
03
Las personas toman la decisión finalRevisión, excepciones y prestación del servicio
SISTEMA / 01
La IA atiende la llamada. Tu equipo se encarga de lo que sigue.6 etapas conectadas
El software prepara · 01–04 Las personas deciden · 05–06
Etapa seleccionada
El precio viene de la lógica de tarifas del negocio. La conversación no inventa el precio.
El registro en esta etapa
Solicitud
Pregunta entrante
Reserva
Aún no preparada
Siguiente responsable
Agente de IA
Solicitud
Detalles del viaje
Datos pendientes
Aún falta una respuesta
Siguiente paso
Cálculo de tarifas
Fuente del precio
Reglas de tarifas del negocio
Disponibilidad
Debe verificarse
Siguiente paso
Autorización de la tarjeta
Acción de pago
Autorizar fondos
Cobro
Una acción aparte
Siguiente responsable
Persona revisora
Decisión
Decide una persona
Excepciones
Disponible para revisión
Siguiente responsable
Equipo de operaciones
Responsable
Equipo humano
Contexto
Conversación + reserva
Proyectos
Coordinar la prestación del servicio
Rechazar antes de improvisar.Cuando el sistema no puede verificar una respuesta, la pregunta pasa a una persona.
Cuando termina la certezaEl sistema tiene un punto de parada.Seis condiciones. Seis respuestas deliberadas.
G1
La disponibilidad no está confirmadaMantén la reserva sin confirmar. Pide a una persona que verifique la capacidad.
Sin inventar disponibilidad
G2
Falta un resultado de pagoConsulta el estado del proveedor de pagos. Una conversación no puede marcarlo como pagado.
El proveedor define el estado
G3
Falta configuración del negocioHaz visible lo que falta. Detén la consulta en lugar de sustituirlo por un valor predeterminado.
Lo desconocido sigue siendo desconocido
G4
Se vuelve a intentar la misma acciónIdentifica la solicitud original antes de repetir una acción externa.
Evitar duplicados
G5
Un servicio externo tarda demasiadoDeja de esperar cuando venza el plazo. Devuelve el error para decidir el siguiente paso.
Tiempo límite explícito
G6
El modelo afirma que algo es ciertoVerifica el registro del negocio antes de que esa afirmación permita ejecutar una acción.
Verificar antes de actuar
01 / Semántica · lo que es cierto
Un registro compartido.
La misma reserva, consultada por personas y agentes.
ClienteReservaVehículoPago
02 / Cinética · quién puede actuar
Una sola verificación de permisos.
PersonaAgente de IALas mismas reglas de acceso
Ninguno tiene una copia privada de la realidad ni un atajo para saltarse los permisos.
03 / Libros de reglas · políticas del negocio
Cambia la regla en un solo lugar.
Las políticas de cada cliente viven fuera del prompt y del flujo de trabajo.
AnticiposHorario de atenciónExcepciones del negocio
Ilustración de la arquitectura. Una retención en la tarjeta no es un cobro. Las personas siguen a cargo de la revisión y la prestación del servicio.
Explora cualquier etapa
01 / La operación
La IA recibe la llamada. El sistema prepara la reserva.
Quien llama habla con un agente de IA. El software consulta tarifas, prepara una cotización y registra la reserva y la retención en la tarjeta para que el equipo las revise.
Cada paso tiene una función, un registro y un responsable claro para lo que sigue.
Desplázate para explorar el sistema
02 / Los límites
Una respuesta incorrecta dicha con seguridad sale cara.
El agente necesita poder detenerse. No puede inventar disponibilidad ni tratar una promesa verbal como un pago realizado.
Seis límites mantienen las decisiones del negocio vinculadas a lo que el sistema puede verificar.
03 / La base
Una misma información. Para personas y agentes.
La reserva, los permisos y las reglas del negocio viven fuera de la conversación. Las personas y los agentes trabajan con el mismo registro.
Las políticas del negocio cambian en un solo lugar. No hay que reescribirlas en cada prompt.
En algún momento clasifiqué 168 proyectos de GarageBand y Logic en cuatro carpetas: Bueno, Malo, Meh y Magia. Resulta que el 65% de los archivos con tonalidad están en la menor o do mayor. Sí. Me siento descubierto.
Llevo más de 25 años tocando guitarra. Improviso blues y rock espacial, juego con música electrónica, estudio porque lo disfruto y, en general, sigo lo que me dé dopamina en el momento.
Bruno es mi Sheltie tricolor de un año. Su nombre imperial completo es Brutus Maximus Aurelius. Está acostumbrado a las caminatas largas. Lo amo.
