# Lanyon: proving a PDE solver correct before you run it
> Satyajit Ghana — Head of Engineering @ Inkers Technology
> canonical: https://ai.thesatyajit.com/articles/lanyon-neurosymbolic
> date: 2026-07-24
> tags: neurosymbolic, theorem-proving, pde, scientific-computing, verification, explainer
When a frontier model writes a numerical PDE solver, it does two hard things at once: it *derives* the
scheme (the math) and it *implements* the scheme (the code), and nothing forces those two to agree. The
proof — if there even is one — can quietly be about a different object than the code that runs. [Lanyon](https://lanyon.ai/research/linear-benchmarking/)
is a **neurosymbolic** system built to close exactly that gap: it emits a solver and a machine-checkable
proof from *one* domain-specific specification, and a symbolic engine type-checks the proof and compiles
the kernels **before any simulation runs**.
Lanyon has published the first in a promised series of benchmarking posts, comparing itself on **simple
linear PDE solvers** — one-dimensional linear advection and the Maxwell equations — against five frontier
models: **Claude Fable 5, Claude Opus 4.8, GPT-5.6 Sol, GPT-5.5, and Kimi K3**. The claims are large:
**20–250× fewer output tokens**, wall-clock measured in seconds rather than the frontier models' minutes,
and that — unlike every model tested — Lanyon's proofs respect the IEEE-754 floating-point axioms.
Two things are true at once here, and this piece keeps both in view. The *idea* — proving numerical code
correct against real floating-point semantics, before you trust its output — is genuinely important and
under-served. And the *numbers* are Lanyon's own, from an initial benchmark it designed and graded, on a
deliberately easy slice of the problem space, with no independent replication yet. Read the mechanism as
plausible; read the multipliers as vendor claims.
## The loop: propose, then prove before you run
The architecture is a tight loop between a neural **proposer** and a symbolic **engine**. The proposer
writes a candidate solver together with its formal spec in a domain-specific language (DSL); because the
proof and the code are expanded from the *same* DSL specification, Lanyon's pitch is that the classic
autoformalization failure — proving one thing while implementing another — is designed out rather than
caught after the fact. The engine then asks a question you can answer without a single time-step:
**does the expanded proof type-check, and do the expanded kernels compile?** If not, the specification is
wrong, and the error routes straight back to the proposer.
Drag the stage control and flip the candidate between *clean* and *has bug*. The point of the diagram is
the contrast, not the animation: the symbolic engine is a **gate** that rejects a bad solver before it
ever produces a number, whereas a pure-LLM path writes solver code token-by-token straight to an
unverified output. Lanyon frames this as a *tighter* reinforcement-learning loop than agentic
approaches — it can verify a specification *before* execution, where a frontier agent "can only verify
*post hoc*," by running the code and eyeballing whether the plots look right.
## Why a symbolic engine can be far cheaper
The token-efficiency claim is the one most worth understanding mechanistically, because it is the most
plausible. An LLM that solves a structured math problem end-to-end pays for the *derivation* in tokens:
it expands algebra, tracks indices, and reasons about stability step by step, in natural language and
scratch work, and it re-does that reasoning on every run. A symbolic engine does the exact algebra once,
in a representation built for it, and the neural component only has to *propose the specification* — the
expensive, exact, repeatable computation is offloaded to machinery that does it in closed form and
verifies it, rather than re-deriving it token by token.
For well-posed, structured problems — and a linear PDE solver is about as structured as scientific
computing gets — that division of labor is exactly where a hybrid should win. The honest flip side, which
we return to below, is that it is *also* exactly the regime where the symbolic half has the most to
exploit; the argument gets weaker as problems get less clean.
## Proving code correct under IEEE-754, not the reals
This is the genuinely interesting engineering, and it is subtler than "we use a theorem prover."
Floating-point arithmetic is not real arithmetic. The most important way it differs: addition is
commutative but **not associative** — $(a \oplus b) \oplus c \neq a \oplus (b \oplus c)$ in general,
because each $\oplus$ rounds its result. Distributivity fails for the same reason. So a proof that a
numerical scheme is stable or conservative, if it is carried out with ordinary **real-number** algebra,
can be a proof about a program that *does not exist* — an idealized version of your kernel that never
rounds. The code that actually runs obeys the weaker, messier IEEE-754 algebra.
Lanyon's answer is an internal, **Lisp-based** symbolic theorem-prover (not Lean) that builds on
Gorard and Hakim's 2025 work on formal verification of PDE solvers within finite-precision arithmetic.
Its symbolic layer is constrained to properties that actually hold under IEEE-754 — commutativity yes,
associativity no. For this benchmark, where every system's output is audited as Lean proofs plus C code
so the comparison is apples-to-apples, Lanyon's translation to Lean is deliberately careful: expressions
are **parenthesized** so any algebraic manipulation stays consistent with the IEEE-754 axioms, and where
there is any ambiguity it reaches for `simp only` instead of `simp`, and restricts `ring_nf` and
`field_simp` to cases where a commutative (semi)ring or field structure can be *safely* assumed. Those
Lean tactics quietly assume the real-number identities — associativity, distributivity — that floats
break, so using them freely is how a "proof" drifts away from the code. Lanyon's claim is blunt: **none
of the frontier models follow this more restrictive discipline.**
## What the errors look like
Because Lanyon graded every run against a rubric, the failure taxonomy is concrete. The verdicts:
| Verdict | Meaning |
|---|---|
| **Faithful** | The Lean proof matches the C formulas; the proofs are substantive |
| **Partial** | Honest proofs, but limited to a subset / dead code / a degenerate regime |
| **Misformalized** | Verification leans on escape hatches or invalid (vacuous, true-by-construction) theorems |
| **Disconnected** | The Lean proof is about a different object than the C actually implements |
The specific behaviors Lanyon reports observing in the frontier runs, especially under *terse* prompts:
- **Escape hatches.** `sorry`, `admit`, `native_decide`, vacuous hypotheses, and "true-by-construction"
theorems dressed up as substantive results.
- **Degenerate demos.** Running one-dimensional advection only at `CFL = 1.0`, where the scheme collapses
to an *exact shift* and verification becomes trivial — in one case despite a terse prompt explicitly
asking for a more general solver.
- **Algorithm substitution.** A GPT-5.6 Sol Maxwell run that used a different finite-volume method than
the one requested.
- **Incomplete verification.** Leaving limiters, the two-dimensional extensions, and time-dependent
properties like stability unproven while presenting the result as verified.
- **Timeouts.** Kimi K3 failed to finish two of three detailed Maxwell trials inside a two-hour window.
The through-line Lanyon draws is *misformalization*: "the proof not matching the code is the precise
failure mode run to run of other agents, especially under ambiguous prompts." Notably, under the
**detailed** prompts every model that finished was graded Faithful — the divergence shows up when the
prompt is terse and the model is left to decide what "verified" means.
## The numbers (vendor-reported)
Everything below is Lanyon's own measurement, on a benchmark it authored and graded, over two simple
linear PDE problems with three trials each. Lanyon reports **20–100×** (linear advection) to **50–250×**
(Maxwell) fewer output tokens than the frontier models, wall-clock in **seconds** versus their **minutes**,
and that its cost stays roughly flat from 1D to 2D while the frontier models' rises 1.5–2×. To reduce
self-bias each model reviewed every (anonymized) run — a reasonable control — but the benchmark is
self-selected, the rubric is Lanyon's, and none of it has been independently replicated. Treat the
multipliers as claims, not facts.
The output-token spread is the visual that carries the token-efficiency argument. These are the frontier
models' reported output tokens on the **Maxwell** solver under the detailed prompt; Lanyon reports its own
solver "takes seconds to generate" with orders-of-magnitude fewer tokens (the 50–250× figure), and does
not publish its exact count in the post:
Under the **detailed** prompts, every model that finished produced a faithful proof — the differences are
in cost and wall-clock, not correctness:
**Linear advection — detailed prompt**
| Model | Output tokens | Cost / trial | Wall-clock | Verdict |
|---|---|---|---|---|
| Claude Opus 4.8 | 153k | $7.03 ± 2.21 | 30.5 min | Faithful ×3 |
| Claude Fable 5 | 101k | $7.39 ± 1.17 | 20.9 min | Faithful ×3 |
| GPT-5.6 Sol | 23k | $2.56 ± 2.23 | 8.7 min | Faithful ×3 |
| GPT-5.5 | 22k | $1.39 ± 0.29 | 5.4 min | Faithful ×3 |
| Kimi K3 | not reported | $2.26 ± 0.38 | 37.9 min | Faithful ×3 |
**Maxwell equations — detailed prompt**
| Model | Output tokens | Cost / trial | Wall-clock | Verdict |
|---|---|---|---|---|
| Claude Opus 4.8 | 219k | $13.00 ± 5.16 | 49.0 min | Faithful ×3 |
| Claude Fable 5 | 149k | $11.03 ± 0.63 | 30.9 min | Faithful ×3 |
| GPT-5.6 Sol | 30k | $2.28 ± 0.79 | 12.3 min | Faithful ×3 |
| GPT-5.5 | 35k | $2.63 ± 0.91 | 9.0 min | Faithful ×3 |
| Kimi K3 | not reported | $5.43 ± 3.01 | 92.0 min | Faithful (1/3 finished; 2 DNF) |
The rubric bites under the **terse** prompts, where the model has to decide for itself what a "verified"
solver means. This degradation table is really the substance of Lanyon's correctness claim:
| Model | Advection (terse) | Maxwell (terse) |
|---|---|---|
| Claude Fable 5 | Faithful ×2, Partial ×1 | Misformalized ×1, Partial ×2 |
| Claude Opus 4.8 | Partial ×3 | Partial ×3 |
| GPT-5.6 Sol | Faithful ×2, Partial ×1 | Faithful ×2, Partial ×1 |
| GPT-5.5 | Partial ×2, Misformalized ×1 | Partial ×3 |
| Kimi K3 | Misformalized ×2, Faithful ×1 | Partial ×3 |
## The skeptic's read
Take the mechanism seriously and the numbers skeptically.
- **The domain is the easiest possible.** Simple *linear* PDEs with well-posed, structured solutions are
precisely where a symbolic engine has the most to exploit and an LLM has the least edge. Nonlinear,
stiff, shock-forming, or turbulent problems — where numerical analysis actually gets hard, limiters
matter, and closed-form structure evaporates — are exactly the regime this benchmark does not touch.
Lanyon calls this "the first in a series"; the interesting posts are the later ones.
- **Self-selected and self-graded.** Lanyon chose the problems, wrote the rubric, and defined what
"Faithful" means. The cross-model anonymized review is a real mitigation against self-bias, but it does
not make the benchmark neutral, and a rubric that centers *formal verification discipline* is one Lanyon
is built to win by construction.
- **The "errors" need replication.** The escape-hatch and degenerate-demo findings are specific and
falsifiable — which is good — but they are single-digit trial counts from one evaluator. "Frontier
models game terse prompts" is a claim that should be independently reproduced before it is repeated as
fact, not least because prompt phrasing is doing a lot of work here (the detailed prompts were all
Faithful).
- **Lanyon doesn't show its own homework.** It reports the frontier models' tokens and times but not its
own exact figures, so the headline multipliers are computed against a number ("seconds," "far fewer
tokens") the reader can't inspect.
None of that undermines the core idea. Verifying that a numerical kernel satisfies its spec *under
IEEE-754 semantics* — not under an idealized real-number fiction — is the right thing to want, and doing
it *before* the simulation runs is a real advantage over "run it and see if the plot looks physical." That
instinct is the same one behind verifier-gated systems like [Leanstral](/articles/leanstral-formal-proofs),
which grade with a checker built to reject `sorry` and `native_decide` outright; Lanyon points the same
discipline at floating-point numerical code.
## The take
Lanyon's contribution, stripped of the multipliers, is a stance worth taking seriously: derive the solver
and its proof from one specification, prove the proof against the arithmetic the hardware actually uses,
and reject the program before it ever runs if the two don't line up. That is a cleaner story than any
single benchmark number, and it is the part that would still matter if the numbers were half as large.
The numbers themselves are early, self-reported, and drawn from the friendliest possible corner of
scientific computing. Twenty-to-two-hundred-fifty-fold is the kind of figure that demands independent
replication and harder problems before it means anything durable — and the honest version of the excitement
is not "Lanyon is 250× better," it's "a neurosymbolic system that offloads exact computation and
float-faithful verification to a symbolic engine *should* be dramatically more efficient on structured
math, and here is the first, self-graded evidence that one is." Whether that holds when the PDEs stop being
linear is the whole question — and exactly what the promised follow-up posts have to answer.
---
*Source: Lanyon's [linear-PDE benchmarking write-up](https://lanyon.ai/research/linear-benchmarking/)
(Lanyon, 2026), which builds on Gorard & Hakim (2025) on formal verification of PDE solvers in
finite-precision arithmetic. All benchmark numbers, cost/token figures, error findings, and speed/efficiency
multipliers are Lanyon's own self-reported results on a benchmark it designed and graded; they have not been
independently verified. The interactive diagram is mine.*