$10.6 million fundraising round led by Dimension backs a team of world-leading Princeton mathematicians and physicists building a radically new kind of scientific AI backed by mathematical proofs of correctness.
, /PRNewswire/ — Lanyon AI, a fundamental research lab developing a new kind of scientific and technical AI, has emerged from stealth following a $10.6 million initial fundraising round led by Dimension, with participation from Industrious Ventures. Lanyon AI is targeting hard sciences: physics, engineering, GPU kernel optimization, frontier AI inference, and other mission-critical tasks, for which correctness is non-optional and mathematical precision is paramount.
In seconds, Lanyon’s AI agent, simply called Lanyon, can conjure simulations of complex physical systems, prove sophisticated mathematical theorems, and invent new state-of-the-art algorithms, with only a tiny fraction of the token and compute cost of frontier models like GPT-5.6 and Fable 5. Even more remarkably, unlike any other AI agent currently available, any code or data generated by Lanyon is provably correct by its very construction: it is mathematically impossible for Lanyon’s generated code not to match its formal specification.
Correctness by construction sounds like a miracle, but it is a natural consequence of Lanyon’s internal mathematical structure. “In 2026, why are agents still reasoning and coding in imperfect human languages?” asks Jonathan Gorard, Lanyon AI’s co-founder and CEO, “Why not have the agent read, write, and reason in a unified formal language, from which implementations and proofs of correctness can be generated simultaneously?”
Many AI companies have proposed a workflow of “autoformalization,” wherein an LLM generates a formal proof of correctness for a piece of code using a proof assistant language such as Lean. According to Gorard, such approaches are clever, but they carry the fundamental risk of misformalization, where the code and the proof don’t actually match. “Instead, what we’re pioneering at Lanyon AI is a neurosymbolic approach: having the LLM do what it’s good at – being creative and proposing interesting ideas – while exploiting symbolic methods to do what they’re good at – being unfailingly reliable and predictable.” The LLM generates a specification, and then reliable symbolic methods expand that specification into code and proofs simultaneously. If the specification cannot be rigorously proven to be correct, the code simply doesn’t generate, and Lanyon loops back to try again until it can.
Lanyon’s formal specification language has another key advantage: because it is highly condensed and domain-specific, Lanyon is not only 100% reliable, but is also extremely fast and low-cost compared to existing frontier models.
“LLMs have transformed software development and have begun making waves in formal mathematics.”, says Simon Barnett, Partner and Head of Research at Dimension, “Despite headlines featuring Olympiad-level proofs and eye-watering benchmark scores, next-token prediction still ends at ‘mostly right’, a standard that doesn’t clear the bar for flight controls, nuclear systems, or simulating chip tape-outs. This is why we’re incredibly excited to support the Lanyon team as they translate their decades of formal methods expertise into neurosymbolic DSLs that ensure alignment between an engineer’s intent, the task’s formal spec, as well as the generated math and execution code. Tomorrow’s hardest physical problems demand explicit guarantees of correctness.”
Lanyon AI is initially targeting critical industries such as aerospace engineering, space and atmospheric propulsion, and nuclear energy, where high-precision and trustworthy computational simulations are essential. “Formally verified, high-accuracy simulations are critical for solving deep scientific and engineering problems”, says Ammar Hakim, Lanyon AI’s co-founder and CTO. “Lanyon unlocks creativity and expands the scope of the solutions accessible to science and technology companies as they tackle some of humanity’s toughest challenges.”
Lanyon AI was co-founded by Jonathan Gorard, Ammar Hakim, and James (Jimmy) Juno, all formerly of Princeton University and/or the Princeton Plasma Physics Laboratory. Gorard is an award-winning applied mathematician, known previously for co-founding the Wolfram Physics Project with Stephen Wolfram. Hakim is a world-leading computational physicist, with deep expertise in fluid mechanics, nuclear fusion, and aerospace engineering. Juno is a leading plasma physicist, having developed cutting-edge methods for some of the hardest problems in laboratory, space, and astrophysical plasmas. The founding team has over five decades of expertise between them, spanning applied mathematics, computational physics, and scientific AI.
Lanyon AI Inc.
Formal verification for a computable universe
100 Overlook Center, Suite 2145
Princeton, NJ 08540
Press Contact: Brian Golden
[email protected]
SOURCE Lanyon AI Inc.
