AI FOR SCIENCE · INTERVIEWS
Gorard says AI took off in code and mathematics because both have verifiers a machine can run, compilers and Lean, while physics, chemistry and biology have no matching verification pipeline. His company, Lanyon AI, is building a language for AI to reason about science in, to make physics 'executable' the way code is.
Lanyon's site gives the direction and the closed first round but not the founder's reasons. The interview adds why he left Princeton, what the product is today (a purpose-built reasoning language attached to an LLM), which two of the three layers of verification the company starts with, and that the experimental layer has just been staffed and not yet built.
No benchmark scores, no experimental link and no round size are given; 'executable physics' today covers mathematical and theoretical consistency, and the experimental layer is, in his words, the hardest and one not yet seriously grappled with. The site promises benchmarks against frontier models and its research notes list comparison pages, which this page did not open.
Gorard says recent gains have come mostly from post-training and reinforcement-learning environments, which is to say from how good the verifiers are. Software has compilers and type checkers and mathematics has proof assistants such as Lean, so coding and maths took off first; physics, chemistry, biology and engineering 'kind of' have none. He traces it to Hilbert: the decision problem produced the theory of computation, a formal language for mathematical reasoning, while Hilbert's matching problem for physics is unsolved. Robin Gandy, Turing's one official student, wrote the nearest attempt in his doctoral thesis, and it did not work.
“We want to make physics executable in the same way that software is executable and that now increasingly mathematics is executable.”Jonathan GorardThe first layer is mathematical self-consistency, already at least as hard as formalising mathematics; the second is consistency with existing physical principles (energy conservation, thermodynamics, covariance), where many heuristics hold only in some regimes, a 'mushier' reasoning he says has not yet been correctly formalised; the third is agreement with physical reality, which 'utterly dwarfs' the first two because every observation carries theory: he puts 20 to 50 layers of theoretical assumption behind 'I detected a particle'. Lanyon starts with the first two and has hired someone, starting in a couple of weeks, to connect it to experimental apparatus.
Today's Lanyon agent is an LLM wrapped in a harness that reasons not in English or Lean but in a compact, purpose-built language for physics and science; his analogy is a type system for physics that can check energy conservation, thermodynamic stability and convergence order. The language expands deterministically into implementation and proof, so the two cannot drift apart, which is the misformalisation risk. He says the company is not competing with the big labs on compute or post-training and mostly builds languages, not models; swapping the LLM for a diffusion model in limited experiments degraded performance 'quite a bit', but not as much as he expected.
Restricting the AI to a few human-readable primitives makes output easy to read, but the reasoning can run to a hundred thousand steps no person can hold; the more expressive the language, the further it drifts from what people understand. Lanyon wants a middle point, neither betting everything on capability nor requiring everything to be auditable by a person. He holds that an AI solving a problem and handing the understanding to a person are separate, and that he himself must rework a proof to understand it, so he argues against using an LLM for that step.
He says the turning point was March 2026, when Math Inc. released a fully AI-formalised proof of Maryna Viazovska's sphere-packing result; in January he had thought that would not happen before late 2027. He then worried about how basic research is defended: 'science as process' (curiosity) has long been justified by 'science as product' (cure cancer, fusion), and once AI can do the product, nobody funds the process. He and his co-founders pitched the idea to funding agencies as an academic project and, he says, were either not answered or rejected, decided to start a company in early June (the company's blog dates its emergence from stealth to July). His colleagues' reactions showed no clear pattern, only a weak one by age: the youngest and the most senior adopted fast, the middle generation was likeliest to say it does not work.
“The timelines were completely wrong.”Jonathan GorardHe agrees with the host that experimental physicists are safe for now because building physical things has inertia. He says he grieves for part of physics, but holds that a discipline is defined by its methods and motives, not its content: how physics is done will be transformed by AI, the aim of building robust models of reality will not. One thing he wants from the company is automated discovery of new description languages, in the manner of Hamilton's mechanics, leaving people the part that is fun.
The timeline has no Lanyon AI entry and /funding does not list it. Lanyon's site (read 2026-10-14) gives a July emergence from stealth, a first round led by Dimension with Industrious Ventures and the angel investor Siqi Chen, and benchmark pages against frontier models.
Gorard adds the founder's reason (funding proposals went unanswered), the product's structure (an LLM plus a purpose-built reasoning language), which layers of verification the company starts with, and the co-founder split (Ammar Hakim is CTO). No round size appears in the interview or in the parts of the site read.
The timeline records OpenAI's Navier–Stokes claim (8 September), the credit dispute (the same day), the Clay Institute's statement (11 September) and the 722 manuscripts of 6 October; it has no entry for Math Inc.'s March release of the formalised sphere-packing proof.
Gorard says that Math Inc. release is what changed his timelines, and that its backstory, involving a PhD student and Jeremy Avigad's group, is more complicated than he knew at the time; he does not rule on it. He reads the Navier–Stokes dispute as an old problem, who gets the credit for the last step, that AI has made impossible to avoid.
The timeline records the launch of the Genesis Mission (24 November 2025).
Gorard says the Department of Energy was then pushing proposals to the Genesis Mission and that the pitches he saw from colleagues 'would have been fine machine learning projects 10 years ago'; his own proposals went to funding agencies he does not name.
Lila's CTO says only about 5% of science is cheap to verify, so real experiments have to serve as the verifier; Gorard says physics lacks a formal verification pipeline, so he builds a language first. One relies on a lab, the other on a formal language, and both say how far AI goes depends on whether anything can automatically tell right from wrong. That is our reading.
The misformalisation Gorard fears is a proof that does not match its implementation; Lean's creator says in another interview that a proof certifies only the statement people wrote, and that the checker itself can be attacked. Lanyon generating implementation and proof from one source answers the first risk; whether the statement is the right one, and how the experimental layer connects, stay open.
Gorard says the company does not compete on compute and its main product is a reasoning language. The evidence to look for is what the language buys: cheaper or more correct than frontier models on the same problems, and scored by whom.
The Lanyon agent is an LLM in a harness that reasons in a compact language built for physics and science.
Company-reported
Consistent with the company's July post on its method; no evaluation results.
It is building a 'type system for physics' that can check energy conservation, thermodynamic stability and convergence order.
Target
He says current proof assistants cannot; the site's research notes have pages on equation solving and proofs, which this page did not open.
Swapping the LLM for a diffusion model degrades performance 'quite a bit', but less than expected.
Company-reported
He calls these limited experiments and gives no figures.
Restricting the AI to a few human-readable primitives makes output very readable, but the reasoning can run to 100,000 steps.
Company-reported
He uses 'seven primitives' as a hypothetical; the company's own figures are not given.
The link to experimental apparatus is not built: someone starting in a couple of weeks has just been hired to do it.
Target
No timetable and no kind of apparatus named.
Another new hire joining on Monday will lead type-theory work, building analogues of Mathlib, Physlib and SciLean for its physics areas.
Company-reported
A statement of hiring and plans, with no output yet.
In March 2026 Math Inc. released a fully AI-formalised sphere-packing proof of several hundred thousand lines of Lean; the backstory is more complicated than he thought at the time.
Industry context
He relays another party's work and says he cannot rule on what happened; this page did not check it.
The company was decided on in early June and, in his telling, came out of stealth 'a few weeks ago'.
Company-reported
The company's announcement is dated July 2026 and its fundraising post August, more than two months before the release; 'a few weeks' may be loose speech or an earlier recording.
Colleagues' attitudes showed no clear pattern, only a weak one by age: the youngest and most senior adopted fast, the middle generation was likeliest to dismiss it.
Guest's judgment
His impression of the colleagues he met, not a statistic.
Experimental physicists are safe for now because building things has inertia, which physical AI might change.
Guest's judgment
He adds that 'maybe we'll come to regret this prediction'.
The experimental layer must deal with the theory-ladenness of observation, a philosophical problem 'we've not even begun really to grapple with'.
Not yet closed
He places this outside what the company has solved so far.
Whether anyone outside Lanyon checks its benchmarks against frontier models.
Would show up as An outside group rerunning the same problems and reporting tasks, accuracy and cost; the company's own comparison pages do not count.The first time a model's output is compared with observables from a real experimental apparatus.
Would show up as A case naming the apparatus, the quantity compared and the size of the gap, and saying how theory-ladenness was handled.Whether an automatically discovered description language is actually used by physicists.
Would show up as A named phenomenon restated in a new language and someone reaching a new conclusion in it.Read 2026.10.14 The full transcript pasted by the author, labelled Curt and Jonathan, read in full, with sponsor reads skipped; the video was not watched. The release date and the length of about two hours ten minutes come from the episode listing found by search and were not checked on the video page. On the company side, Lanyon's site was read for its company page, the July announcement, the opening of the fundraising post and the research-notes index; the benchmark notes were seen by title only. Open the interview ↗Show's Substack page ↗