Co-founder and CEO @lanyon_ai, making the universe computable. Part-time math/physics research @Princeton Previously @Cambridge_Uni @WolframResearch
Princeton, NJ
- Tweets 1,855
- Following 23
- Followers 47,132
- Likes 1,860
It is an unfortunate reality that people who talk incessantly about themselves and their achievements really do get taken more seriously than those who consider such things to be gauche. I need to stop being surprised by this.
39
35
976
31,218
Jonathan Gorard retweeted
It’s our pleasure to welcome Aanya Bhandari to the Lanyon AI team as a Research Fellow, specializing in frontier model architecture and training.
Aanya joins us following a research fellowship at Princeton University working with our CEO Jonathan Gorard on formal verification for transformer and recurrent neural network architectures. She brings expertise in frontier AI architectures, financial technology, and quantum computing. Welcome Aanya!
3
35
2,297
Consequentialism doesn’t work because it neglects computational irreducibility.
Deontology doesn’t work because it neglects undecidability.
For any sufficiently rich moral world, only virtue ethics can prevail.
The funny thing about ethics is that everything inevitably returns to this basic question: can you solve both the Nazi-at-the-door AND the secret organ-harvesting trolley problem at the same time?
Surprising how often the answer is no.
34
13
306
38,256
Jonathan Gorard retweeted
I am very excited to work with Chris and @getjonwithit on building a type system for all of the physical universe!
It’s our pleasure to welcome Chris Rugenstein to the Lanyon AI team as Founding Member of Technical Staff, specializing in type systems and formal verification.
Chris joins us from the Institute for Defense Analyses and the Department of Energy, and brings deep expertise in pure mathematics, theoretical computer science, and formal methods for type theory. Welcome Chris!
2
19
2,745
Jonathan Gorard retweeted
It’s our pleasure to welcome Chris Rugenstein to the Lanyon AI team as Founding Member of Technical Staff, specializing in type systems and formal verification.
Chris joins us from the Institute for Defense Analyses and the Department of Energy, and brings deep expertise in pure mathematics, theoretical computer science, and formal methods for type theory. Welcome Chris!
3
43
5,782
I wrote a few words about where I think humanity is right now, what has led us to this point, and what I think an optimistic vision for the future (at least for science, mathematics, and technology) might look like.
Link below. 👇
7
8
110
8,039
Jonathan Gorard retweeted
A few words from @getjonwithit on the meaning of the present moment, and what a human-oriented outlook for science, mathematics, and technology may look like in a world of growing AI capabilities.
lanyon.ai/blog/vision/
2
2
25
3,004
Jonathan Gorard retweeted
An electromagnetic wavepacket diffracting over a metal cylinder inside a metal waveguide.
Simulated using a high-order (p=2) discontinuous Galerkin scheme for the perfectly hyperbolic Maxwell equations, autonomously discovered, verified, and implemented with Lanyon.
2
2
61
5,595
Jonathan Gorard retweeted
This sort of thing - speeding up numerical methods - will get way less hype than NS, but will probably have far more eventual economic impact. If you’re wondering how AI math will matter in the real world, it’s stuff like this.
We've been using Lanyon to discover (and prove correctness of) new state-of-the-art discontinuous Galerkin algorithms for solving PDEs.
Just select an order-of-accuracy and (optionally) a polynomial basis, and have Lanyon search the space of possible modal DG algorithms until it finds one that provably works for your problem. Then have it generate an end-to-end proof of correctness, and an optimized implementation, all from the same spec. All in a few minutes, all with negligible inference cost.
It turns out: automated algorithm discovery is a lot of fun!
Come and read more about it in our updated Research Notes, or by visiting our GitHub. 👇
2
4
161
8,496
We've been using Lanyon to discover (and prove correctness of) new state-of-the-art discontinuous Galerkin algorithms for solving PDEs.
Just select an order-of-accuracy and (optionally) a polynomial basis, and have Lanyon search the space of possible modal DG algorithms until it finds one that provably works for your problem. Then have it generate an end-to-end proof of correctness, and an optimized implementation, all from the same spec. All in a few minutes, all with negligible inference cost.
It turns out: automated algorithm discovery is a lot of fun!
Come and read more about it in our updated Research Notes, or by visiting our GitHub. 👇
We've been having a lot of fun using Lanyon to perform automated discovery of new discontinuous Galerkin (DG) algorithms for discretizing PDEs. We're starting with simple linear and nonlinear advection problems, with some more advanced (and exciting!) examples on the way.
The workflow is simple: have Lanyon autonomously explore the space of possible modal DG discretizations (of any order of accuracy), while autonomously checking its work by attempt to prove various correctness properties of the modal reconstruction polynomials, surface terms, and volume integrals, as well as entropy stability properties of the underlying fluxes. Once Lanyon finds a new discretization that works, it generates an optimized implementation in C and starts autonomously running numerical simulations with it. It turns out that you can very quickly discover all kinds of weird and wonderful (but provably correct!) numerical algorithms this way, many of which go beyond the current state of the art. And we're only just scratching the surface of what is possible with formally verified numerics.
Even for these simple cases, the optimized implementations (for p=1 and p=2, i.e. second-order and third-order accuracy) span around 30,000 lines of generated C code and around 40,000 lines of generated Lean proof. But Lanyon completes the whole algorithm discovery task in a few minutes, and with less than a dollar in total inference cost. We've updated our Research Notes with some of these new algorithmic results, but stay tuned for more discoveries still to come. GitHub links and Research Notes below. 👇
3
11
139
21,708
Updated GitHub repositories for the advection-diffusion and viscous Burgers' equations, containing the implementations and proofs for the new DG discretizations:
github.com/lanyonai/Advectio… github.com/lanyonai/BurgersE…
Updated research notes (by @minmodammar) describing this new work:
lanyon.ai/research/advection… lanyon.ai/research/burgers-e…
2
15
1,753
Jonathan Gorard retweeted
We've been having a lot of fun using Lanyon to perform automated discovery of new discontinuous Galerkin (DG) algorithms for discretizing PDEs. We're starting with simple linear and nonlinear advection problems, with some more advanced (and exciting!) examples on the way.
The workflow is simple: have Lanyon autonomously explore the space of possible modal DG discretizations (of any order of accuracy), while autonomously checking its work by attempt to prove various correctness properties of the modal reconstruction polynomials, surface terms, and volume integrals, as well as entropy stability properties of the underlying fluxes. Once Lanyon finds a new discretization that works, it generates an optimized implementation in C and starts autonomously running numerical simulations with it. It turns out that you can very quickly discover all kinds of weird and wonderful (but provably correct!) numerical algorithms this way, many of which go beyond the current state of the art. And we're only just scratching the surface of what is possible with formally verified numerics.
Even for these simple cases, the optimized implementations (for p=1 and p=2, i.e. second-order and third-order accuracy) span around 30,000 lines of generated C code and around 40,000 lines of generated Lean proof. But Lanyon completes the whole algorithm discovery task in a few minutes, and with less than a dollar in total inference cost. We've updated our Research Notes with some of these new algorithmic results, but stay tuned for more discoveries still to come. GitHub links and Research Notes below. 👇
2
3
37
10,980
Physics will be next, and this time we have a chance to learn from the mistakes of math and make the sociology a little less toxic. Let’s not screw it up.
42
79
1,191
84,780
Hmmm... if only there were a tool that let someone define a scientific problem, have AI formally specify a mathematical model for it, automatically verify its correctness properties, and then simulate it autonomously on dedicated compute...
Another prediction: interest will shift toward applied mathematics.
Take a real-world problem you’ve always been curious about. Ask AI to build a mathematical model, include the relevant constraints, and solve it to a useful degree of accuracy.
Compute will remain a major bottleneck. Think of asking whether an astronomically large integer is prime: knowing how to solve a problem doesn’t mean you have the resources to finish the computation.
9
10
150
18,888
We all know what it means to verify a proof. But what does it mean to verify a physics simulation?
Here's a talk I gave back at Princeton back in March 2025, about the beginnings of what would later become Lanyon AI, and the unique challenges of verifying numerics. 👇
Building a formal verification framework for physics and engineering.
A talk by our CEO Jonathan Gorard (@getjonwithit) from March 2025 at Princeton, outlining the beginnings of Lanyon, and the challenges of formally verifying numerical methods:
piped.video/watch?v=8NDcltA5…
3
6
139
11,299