Jonathan Gorard, applied mathematician and co-founder of the Wolfram Physics Project, founded Lanyon AI after a March 2026 breakthrough shattered his timeline expectations: a startup called Math Inc. autonomously produced a complete Lean proof of Maryna Viazovska’s Fields Medal–winning sphere-packing result in 8 and 24 dimensions, years ahead of his predicted 2027–2028 horizon, triggering a personal and professional crisis about the future of curiosity-driven physics and mathematics.
The Sphere Packing Shock
Gorard had spent a decade working on automated theorem proving and believed he understood the difficulty curve; the March 2026 proof arrived as a multi-hundred-thousand-line Lean formalization generated end-to-end by an AI harness, revealing his mental model of AI progress was fundamentally wrong.
The two-year acceleration mattered not because of the technology itself but because academia’s glacial sociology — funding agencies, hiring, PhD pipelines — had zero time to adapt, collapsing the implicit bargain that sustains curiosity-driven research.
Science as Product vs Process
Gorard distinguishes “science as product” (cure cancer, fusion, clean energy — universally fundable) from “science as process” (curiosity-driven work on quantum gravity, turbulence, p-adic Langlands — justified only by laundering it through product promises).
Grant proposals routinely overstate instrumental value; e.g., algebraic number theorists cite cryptography though the relevant math is centuries old, and PDE researchers claim semiconductor applications they don’t actually pursue.
AI decouples output from process: if models can generate the product (papers, proofs, code) without the human process, the societal justification for funding the process evaporates, leaving only hedonistic motivation — “I do it because I like thinking about problems.”
Is Science Just Hedonism?
Gorard admits his own motivation is largely hedonistic; he would enjoy the intellectual work even if disconnected from civilization, a view he suspects is common but rarely voiced.
Unlike artists, whose work provides external enjoyment, research mathematics is an extremely niche “art form” with almost no public audience, making it uniquely vulnerable when instrumental justification disappears.
Perelman’s rejection of the Clay Prize anticipated this: he highlighted the arbitrariness of awarding all credit to the final-step solver, a problem AI exacerbates by automating last-mile problems and destroying incentives for foundational incremental work.
Why Academics Ignored AI
Gorard tried warning Princeton colleagues in early 2026; most were incurious, recycling 2015-era ML project ideas for DOE’s “Genesis Mission” proposals and dismissing LLMs as “stochastic parrots” based on outdated 2021 transformer critiques.
They conflated “this technology is bad” with “this technology doesn’t work,” ignoring the massive post-training stack (RL, tool use, harnesses, diffusion components) driving capabilities.
Mid-career researchers were most resistant — they had built careers on the old model and faced existential threat; early grad students and late-career professors adopted faster.
Why Leave Princeton?
Gorard and co-founder Ammar Hakim pitched their vision — a language mechanizing scientific reasoning the way computation mechanized mathematical reasoning — as an academic project; every proposal was rejected or ignored amid a brutal funding climate.
Seeing peers raise venture capital for similar-scale research, they spun out Lanyon AI in June 2026, moving from stealth to public within weeks.
Turing’s Student and Physics Formalization
The core asymmetry: math and code have formal verification pipelines (Lean, compilers, type checkers) enabling RL with verifiable rewards; physics, chemistry, biology lack an equivalent.
Hilbert’s Entscheidungsproblem birthed computation theory for math; his parallel program to axiomatize physics — mechanizing physical reasoning — remains unsolved.
Robin Gandy (Turing’s only PhD student) attempted this in his 1950s thesis On Axiomatic Systems in Mathematics and Theories in Physics, extending type theory toward an abstract machine for scientific induction, but the project was too ambitious for a thesis and stalled.
Theory-Ladenness of Observation
Physical reasoning has three layers: mathematical consistency (internal logic), theoretical consistency (conservation laws, covariance, unitarity — often approximate or regime-dependent), and experimental consistency (interface with reality).
The experimental layer hits philosophy-of-science limitative results: Hanson and Kuhn showed observations are theory-laden both semantically (“I detected a particle” presupposes 20–50 theoretical layers) and perceptually (optical illusions demonstrate perception depends on mental models).
Automating experimental verification requires parameterizing over the theoretical apparatus assumed in any measurement — a complexity absent in math and pure theory.
Why Math Isn’t Enough
Axiomatic QFT proponents might claim physics reduces to math, but fundamental theories are massively under-constraining: Einstein’s equations permit time travel and white holes; Yang-Mills theory has vastly more mathematically consistent variants than nature realizes.
Condensed matter is a partial exception — it can realize arbitrary field theories — but even there, the gap between mathematical possibility and physical actuality is enormous.
Mechanizing only math and theory yields a superset of reality, not reality itself; experimental grounding is essential.
Sapir-Whorf for AI
Lanyon builds a neurosymbolic agent: an LLM constrained to reason in a custom domain-specific language (DSL) for physics, not English or raw Lean.
Bet: reasoning language shapes reasoning capacity (weak Sapir-Whorf). Just as Lean enables superhuman math proofs and Python enables superhuman coding, a physics-optimized DSL should enable superhuman physical reasoning.
The DSL is intentionally condensed (fewer tokens), precise (sharper delineations), and interconvertible with formal proofs and executable simulations, eliminating the “misformalization” gap where an LLM’s English reasoning doesn’t match the code it writes.
Filtering the Paper Deluge
arXiv floods (thousands of papers/week) and LLM-generated “theories of everything” have jammed the social contract of peer review; unlike code (runnable) or math (formalizable), physics papers lack an executable verification layer.
Lanyon’s goal: make physics executable — check theoretical consistency, thermodynamic stability, numerical convergence, and eventually experimental agreement — so AI-generated hypotheses can be automatically culled.
Executability ≠ understanding; Gorard argues understanding requires cognitive friction (re-deriving proofs oneself), and LLMs may hinder rather than help human learning if they remove that friction.
Can AI Transmit Understanding?
An LLM solving Navier-Stokes may “understand” it internally, but transmissibility to human brains is a separate, unsolved problem.
LLMs reason natively in latent spaces (e.g., “GibberLink” dial-up tones) incomprehensible to humans; forcing them into human-auditable chains of thought may require exponential translation overhead.
Lanyon’s DSL approach constrains the LLM to human-comprehensible primitives (Toki Pona minimalism), but expressive power trades off against interpretability: 100,000 simple steps exceed human working memory, while compressed high-level steps become opaque.
Must AI Be Embodied?
Even mathematics may ultimately require embodiment: our mathematical intuitions (quantity, geometry, topology) originate from primate sensorimotor interaction with the world (Piaget); a disembodied intelligence would develop alien representation languages.
Wolfram/Gorard’s axiomatic exploration found structures intuitive to LLMs but utterly opaque to humans.
For experimental physics, embodiment is unavoidable: Lanyon is hiring to connect its reasoning engine to automated labs, confronting the “shim problem” — mapping model observables to real instrument outputs while accounting for theory-ladenness.
Mysteries Are Description Language Artifacts
Gorard’s philosophical stance: apparent fundamental mysteries (wave-particle duality, black hole thermodynamics) are artifacts of using the wrong description language.
Lagrangian vs Hamiltonian mechanics: mathematically equivalent, philosophically opposite (local vs teleological); thermodynamics becomes trivial in computational/information-theoretic language but mysterious in PDE language.
AdS/CFT: black hole area laws are mysterious in bulk gravity but trivial boundary thermodynamics.
Lanyon aims to automate discovery of new description languages — “automated William Rowan Hamilton” — that bypass current bottlenecks while remaining human-accessible.
Grieving Physics
Gorard grieves the romanticized “natural philosopher” ideal (inkwell, fundamental equations) already lost to modern computational grind (debugging Mathematica, matplotlib); AI accelerates this loss.
Colleagues enthusiastically offloading equation-solving and coding to Claude “take all the fun out” — the enjoyable part is the friction of thinking.
Coping strategy: build the AI tool he would want — automate the Hamilton-level description-language discovery he can’t do, preserve the exploratory play he enjoys.
What’s Left for Physicists?
Content-level work will transform radically; methodology and motivation (building robust quantitative models of reality) will persist, as they have from Babylonian surveyors to Newton to modern condensed matter.
Historical precedent: pre-Socratics would have seen calculus as field-ending, yet physics survived by adopting the new language; AI is the next such revolution.
The Next Description Language
Elevator pitch: history shows progressive revolutions in description languages (natural language → geometry → analysis → computation), each resolving the previous era’s mysteries by revealing them as language limitations.
AI capabilities are now bottlenecked by description languages; unless we build the next formal language for physical reasoning — completing Hilbert’s/Gandy’s dream — we get either capability stagnation or “slopification” (unverified hypothesis explosion).
Verification pipelines require the right description languages; that is Lanyon’s core bet.
Spacetime Discreteness and Beacons
Pre-Lanyon, Gorard worked on observational signatures of spacetime discreteness in high-energy astrophysics (strong gravity amplifying Planck-scale structure into testable signals).
With Ammar Hakim, developed formal verification for physics: proof assistants for PDE solvers hit novel issues — thermodynamic consistency, L2 stability, floating-point arithmetic (IEEE 754 axioms) — requiring new tooling beyond Lean/Agda.
Led the BEACONS project: using category theory and approximation theory to compose small, provably correct neural networks into deep architectures while preserving explainability — abandoned when the March 2026 shock made academic timelines implausible.
