Lanyon AI, a fundamental research lab, has emerged from stealth with a $10.6 million funding round to advance its novel scientific artificial intelligence. The round was led by Dimension with participation from Industrious Ventures, backing a team of Princeton mathematicians and physicists. The company is developing an AI capable of generating code and data that is mathematically guaranteed to be correct, targeting mission-critical scientific and technical fields.
A New Standard of AI Correctness
The company's agent, named Lanyon, can generate complex physical simulations, prove mathematical theorems, and devise new algorithms with remarkable speed and efficiency. Unlike frontier models, Lanyon operates at a fraction of the token and compute cost. Its most significant innovation is that any output it produces is provably correct by its very construction, eliminating the possibility of error.
This guarantee of correctness stems from the AI's unique internal mathematical structure. Co-founder and CEO Jonathan Gorard questions why current AI agents still rely on imperfect human languages for reasoning and coding. Lanyon instead operates within a unified formal language, allowing it to generate implementations and proofs of correctness simultaneously and flawlessly.
Pioneering a Neurosymbolic Method
Lanyon AI pioneers a neurosymbolic approach that diverges from common industry practices like "autoformalization". Gorard notes that attempting to formally prove code after it has been written carries a fundamental risk of "misformalization," where the proof and the code do not align. Lanyon's method avoids this pitfall by integrating the creative and logical steps from the outset.
The system leverages a large language model (LLM) for its creative strengths, tasking it with proposing interesting ideas as a formal specification. Reliable symbolic methods then take over to expand that specification into both code and a corresponding proof at the same time. If the specification cannot be rigorously proven correct, the code is not generated, and the agent re-evaluates its approach.
Targeting Mission-Critical Industries
This technology has attracted significant investor confidence due to its applicability in high-stakes domains. Simon Barnett, Partner at Dimension, emphasized that for flight controls, nuclear systems, or chip simulations, the "mostly right" standard of typical AI is insufficient. He expressed excitement for Lanyon's ability to ensure alignment between an engineer's intent and the final execution code.
Lanyon AI is initially focusing on industries where precision is paramount, including aerospace engineering, space propulsion, and nuclear energy. Co-founder and CTO Ammar Hakim stated that formally verified, high-accuracy simulations are critical for solving deep scientific and engineering problems. He believes Lanyon will unlock creativity and expand the scope of solutions for humanity's toughest challenges.
A Team of Scientific Experts
The company was co-founded by a team with deep roots in academia and advanced research, all formerly of Princeton University or the Princeton Plasma Physics Laboratory. The founders include applied mathematician Jonathan Gorard, computational physicist Ammar Hakim, and plasma physicist James Juno. Together, they bring over five decades of combined expertise in applied mathematics, computational physics, and scientific AI.
With its successful funding round and innovative technology, Lanyon AI is positioned to redefine the role of artificial intelligence in science and engineering. By delivering a fast, efficient, and provably reliable tool, the company addresses a critical need for certainty in fields where errors are not an option. This new paradigm of correctness by construction could accelerate breakthroughs in humanity's most complex and vital endeavors.