Lanyon AI revela una ronda de $10.6 millones para lograr que el código de física se demuestre por sí mismo

Why it matters

Lanyon AI is betting that scientific AI will be sold on verifiability rather than fluency. The hard part is proving that a formal specification reflects what an engineer intended.

Jonathan Gorard (@getjonwithit), un matemático aplicado que trabajó anteriormente en Wolfram Research y Princeton, está tomando una ruta más reducida hacia el código generado por IA: hacer que el software demuestre que hace lo que dice su especificación formal.

Lanyon AI, que Gorard cofundó con los físicos computacionales Ammar Hakim (@minmodammar) y James "Jimmy" Juno (@JunoRavin), dijo en un comunicado de prensa del 17 de agosto que había salido del sigilo después de cerrar un financiamiento inicial de 10.6 millones de dólares en julio. Dimension lideró la ronda, con la participación de Industrious Ventures y la inversionista ángel Siqi Chen, según el anuncio de Lanyon AI.

El laboratorio con sede en Princeton, Nueva Jersey, está construyendo un agente de IA, también llamado Lanyon, que genera código de simulación científica y las pruebas matemáticas que lo acompañan. Lanyon AI está inicialmente presentando el sistema a los sectores aeroespacial, de propulsión, energía nuclear y otros campos donde una respuesta que parezca plausible sirve de poco si los ingenieros no pueden verificar el cálculo subyacente.

Gorard, Hakim y Juno se conocieron mientras trabajaban en el Princeton Plasma Physics Laboratory, dijo Industrious Ventures en su anuncio de inversión. Sus investigaciones abarcaron entornos de plasma en reactores de fusión y alrededor de agujeros negros. Los registros de Princeton muestran que Gorard se unió en 2024 al grupo de ingeniería de software de investigación para trabajar en Gkeyll, un framework de simulación multipfísico liderado por Hakim.

Gorard tiene un MPhil en computación científica por la University of Cambridge y ocupó previamente cargos en Cardiff University, Wolfram Research y el Wolfram Institute. Lanyon AI dice que ayudó a cofundar el Wolfram Physics Project con Stephen Wolfram. El trabajo de Hakim abarca mecánica de fluidos, fusión nuclear e ingeniería aeroespacial, mientras que Juno se ha enfocado en plasmas de laboratorio, espaciales y astrofísicos.

Ese antecedente precede la propuesta de recaudación de fondos. Gorard y Hakim publicaron en 2025 una canalización de verificación formal para solucionadores de ecuaciones en derivadas parciales hiperbólicas. El trío continuó en febrero de 2026 con BEACONS, un framework para producir solucionadores neuronales con garantías verificables por máquina sobre propiedades que incluyen convergencia, estabilidad y conservación.

Lanyon separa la creatividad de la verificación

La arquitectura de Lanyon AI asigna diferentes tareas a los modelos de lenguaje y al software simbólico. Un LLM propone una especificación en un lenguaje formal específico del dominio. Sistemas deterministas expanden luego esa especificación en código ejecutable en C y pruebas en Lean, un lenguaje de demostración de teoremas. Si el proceso de prueba falla, Lanyon AI dice que la implementación no se genera.

La distinción importa porque pedirle a un modelo de lenguaje que escriba código y, por separado, que produzca una prueba crea otro punto de falla: la prueba puede verificar una especificación diferente de la que el código implementa. El sistema de Lanyon AI deriva la implementación y la prueba de la misma fuente formal.

Ese diseño respalda una garantía más limitada de lo que podrían sugerir las afirmaciones más amplias de Lanyon AI. En su publicación de lanzamiento de julio, Lanyon AI describió inicialmente al agente como matemáticamente incapaz de cometer un error. Una nota al pie matizó esa afirmación: Lanyon AI garantiza que la implementación coincide con la especificación formal, mientras que determinar si la especificación captura la intención en lenguaje natural del usuario sigue siendo un problema de investigación abierto.

El riesgo práctico, por tanto, se desplaza aguas arriba. El código generado puede implementar fielmente una especificación que no expresa lo que el ingeniero realmente quería. El caso técnico de Lanyon AI depende de reducir esa brecha semántica a la vez que preserva las garantías formales que distinguen el producto de los agentes de codificación convencionales.

Lanyon AI ha comenzado a publicar ejemplos a través de su organización en GitHub, incluidos solucionadores verificados formalmente para las ecuaciones de Maxwell, las ecuaciones de Euler compresibles, sistemas de advección-difusión y las ecuaciones de Vlasov electrostáticas. Los repositorios proporcionan código y pruebas en Lean que pueden ser inspeccionados, aunque las comparaciones más amplias de rendimiento y costo de Lanyon AI siguen basadas en benchmarks producidos por Lanyon AI.

Los inversionistas cubren la investigación y las ventas industriales

La alineación de inversionistas se corresponde estrechamente con el problema de los fundadores. Dimension se describe como una firma de inversión orientada a la investigación enfocada en la ciencia y la computación. Industrious Ventures invierte en los sectores aeroespacial, energético, manufactura, seguridad nacional y otros sectores industriales a los que Lanyon AI quiere vender.

Gorard escribió que los fundadores eran "tres teóricos nerds recién salidos de la academia" que necesitaban acceso a clientes en aeroespacial, nuclear y defensa. Industrious Ventures suministra esas relaciones. Dimension le da a Lanyon AI espacio para operar como laboratorio de investigación mientras los fundadores desarrollan un producto comercial alrededor de su trabajo en métodos formales.

Chen proporcionó el dinero inicial. Gorard dijo que la inversión de Chen pagó la primera oficina de Lanyon AI, las computadoras y la asesoría legal durante el resto del proceso de recaudación de fondos.

Los 10.6 millones de dólares le dan a los fundadores tiempo para convertir años de investigación en software de producción y encontrar compradores dispuestos a poner código de simulación generado por IA cerca de sistemas físicos costosos. Lanyon AI ha demostrado que las pruebas pueden generarse junto con el código. Su prueba comercial es si los ingenieros confían lo suficiente en el proceso de especificación como para usar el resultado.