hi, i'm dev. i'm currently building Third Weather, where i'm working on making near-frontier AI models run locally, at practical speeds, on smaller devices. i'm also an Emergent Ventures fellow and a Cosmos Institute grantee.
i love experimenting with autonomous AI systems to see how far they can go in making actual scientific and mathematical progress. lately, i've been working on the Keller–Klein Berry–Esseen conjecture with professor Paata Ivanisvili, and on counterexamples to the Bapat–Lal q-permanent monotonicity conjecture with professor Carlos Martins da Fonseca. you can find my ongoing agentic mathematics experiments here.
i also work on quantum computing tools. i've been a contributor to IBM's Qiskit and am building NoiseVault, an open-source tool for working with real quantum-device noise models across different quantum computing frameworks.
my research spans AI memory systems, model selection and evaluation, and numerical methods for generative modelling. some of my single-authored papers have been accepted to workshops at NeurIPS and within the ACL conference community.
About Me
My legal and administrative name is Dev Goyal. I used this name publicly for a long time, so you may find my work and references to me under Dev Goyal rather than Dev D. Goyal. I've tried to consolidate as much of that work as possible on this website, with links to the original sources.
Pronouns: he/him/his
Currently: making frontier AI models go brr locally, on increasingly smaller devices
Currently (re)playing: Xenoblade Chronicles: Definitive Edition, Metroid Prime 4: Beyond, Pokémon Champions (still haven't hit champion tier 😭)
Some fun facts: world record holder in jump rope, speedcuber, was ranked #1 in competitive pokémon vgc a while back
Recurring side quest: un-smartphonifying the humble mp3 player, de-suckifying camera operating systems, practising forbidden minigame alchemy, eureka-farming with AI agents
Links
X (Twitter): https://x.com/deyvium
GitHub: https://github.com/dvgyl
Hugging Face: https://huggingface.co/deyvium
Contact form: https://dvgyl.com/contact
Grants & Awards
Emergent Ventures, Mercatus Center at George Mason University, 2026. USD $10,000. building tools to explore whether stylus-based drawing kinematics can support non-diagnostic clinical triage for ADHD, autism, and anxiety. https://marginalrevolution.com/marginalrevolution/2026/10/emergent-ventures-india-20th-cohort.html
Cosmos Institute Grant, Cosmos Institute, 2026. USD $6,000. researching how well LLMs preserve human intentions, preferences, and boundaries. https://blog.cosmos-institute.org/p/announcing-80-new-cosmos-grantees
Non-Trivial Fellowship, Non-Trivial, 2025.
Record
Grantee, Cosmos Institute, 2026. researching how well LLMs preserve human intentions, preferences, and boundaries.
Emergent Ventures Fellow, Mercatus Center at George Mason University / Emergent Ventures, 2026. building tools to explore whether stylus-based drawing kinematics can support non-diagnostic clinical triage for ADHD, autism, and anxiety.
Catalyst Programme, 2026.
Indian National Team Representative, International Economics Olympiad, 2025. part of the indian team for the international economics olympiad.
Researcher, Non-Trivial, 2025.
Research
Time-reversal inference with uncertain observation channels: code and supporting data. Dev D. Goyal. Preprint, 2026. A recording can look different forward and backward in time because of the physical source or because its sensors respond differently. We ask when a finite recording can separate these explanations. For stationary Gaussian sources and linear sensors, we prove an ambiguity result. Every finite stationary Gaussian probability law with nonsingular covariance has a reversible-source explanation if source spectra and suitable channel delays are unrestricted. Thus exact finite-record probabilities alone cannot resolve the source in this class. We give two tests that use additional information. Calibrating two sensors bounds the lag asymmetry that their relative phase can create. With three channels, the closure product multiplies their pairwise cross spectra. Its phase, called the closure phase, cancels sensor phase offsets under the specified sampled response model. Both tests also need a covariance envelope for all channels and times to control finite-record error. The closure test needs a further bound on covariance contributions omitted from its estimate. In a simulated Brownian gyrator at equilibrium, unequal sensors produce raw bootstrap detections in 397 of 400 records of length N = 524 289, while the calibrated test rejects none. At that length, the calibrated test detects all 200 records at a fourfold bath-temperature ratio but none at a twofold ratio. These results show both the value of sensor information and the large record lengths that valid tests can require. Finally, rotating sources can have identical sampled laws but continuous-time entropy-production rates that differ without bound. Source inference therefore needs sensor information, while inference about dissipation also needs control of motion between samples. https://dvgyl.com/compendium/research/time-reversal-inference
Certified Model Ranking under Limited Label Errors. Dev D. Goyal. Under review at IEEE TAI, 2026. How many errors in shared test labels can a model ranking tolerate? Correcting one label can affect several comparisons because all models use the same examples. Test-label audits find errors in widely used benchmarks. Current evaluation methods include label audits, statistical confidence assessments, and comparisons between two systems. We study a worst-case question for fixed binary predictions. If only flagged labels may change, how much comparison weight can reverse under a given error budget? Checking comparisons individually can overstate the total reversal weight attainable under a single permitted correction. We construct finite lists that represent every permitted correction within the same error budget. Evaluating a list bounds the largest reversal weight from above and below. One tolerance shifts the accuracy margin used to count reversals. The other allows an additive error in reversal weight. For fixed tolerances, list size and construction cost are polynomial in the input length. Exact certification is coNP-complete even with a fixed margin and reversal-weight limit. A separate polynomial-time certificate tests which pairs of comparisons can reverse together at the requested margin. It gives a lower bound on the minimum number of label changes needed for the reversal weight to exceed the limit. A permitted correction whose reversal weight exceeds the limit gives an upper bound on that number. The tools distinguish a certified comparison rule, a permitted correction that violates it, and an unresolved result. Maintainers can report how many flagged label changes the stated rule provably tolerates. https://dvgyl.com/compendium/research/certified-model-ranking
Accuracy Across Sampling Step Counts in Flow Matching. Dev D. Goyal. Under review at IEEE TAI, 2026. Research on accuracy across different sampling step counts in flow-matching methods. https://dvgyl.com/compendium/research/flow-matching-step-counts
When More Search Can Worsen Deployment: Best-of-N Selection on an Incomplete Proxy. Dev D. Goyal. Accepted to NewInML workshop at NeurIPS 2026, 2026. Can wider search worsen deployment when the selection score omits a cost? Selection overfitting and the effect of trading costs are known concerns. We use standard finite-pool rank probabilities to distinguish changes in winner exposure from the measured gross-to-net outcome gap. In a trading simulation, we rank four pools of 500–1,500 ridge-regression strategies by gross Sharpe, ignoring execution costs. Wider search selects higher turnover, and the capacity component of the gap, from trade caps and price impact, has a positive fitted slope on the primary search grid in all 16 pool-by-capital cells. From one to 32 trials, mean net Sharpe declines in 11 of the 16 cells. In the other five, including all four pool-A cells, mean net Sharpe rises. The capacity component is not statistically established. Its joint selection–evaluation bootstrap interval for pool B at USD 500 million is [−0.022, 0.121]. Mean candidate gross Sharpe is negative in every pool. All tested rules except an infeasible rule that selects on evaluation outcomes have negative mean net Sharpe on the comparison grid. Selecting on modeled net Sharpe improves that mean by 0.430, with paired interval [0.192, 0.723], but leaves it at −0.071. The calculation makes search-induced exposure to an omitted term explicit. Under the same sampling assumptions, it also applies to validation scores that omit serving cost. It also separates this measurement problem from selection noise. Statistical correction cannot recover a cost the score does not measure. https://dvgyl.com/compendium/research/when-more-search-can-worsen-deployment
Tracing False Speaker Links Through Retrieval and Answering. Dev D. Goyal. Accepted oral to NORA workshop at AACL 2026, 2026. Studies how false associations between speakers alter memory retrieval and answers in LLM systems. https://dvgyl.com/compendium/research/false-speaker-links
Projects
Third Weather (2026). Making near-frontier AI models run locally on smaller devices. Optimising model distillation, so that near-frontier AI models run locally, at practical speeds, on smaller devices. Demo: https://www.thirdweather.ai
Frontier Draft (2026). A playful founding-team draft game. A playful founding-team draft game about selecting people for a fictional frontier AI lab within a points budget. Demo: https://www.frontierdraft.app
NoiseVault (2026). An open-source toolkit for quantum-device noise profiles. An open-source toolkit that exports calibration-derived noise profiles to Qiskit, Cirq, PennyLane and Stim. Code: https://github.com/dvgyl/noisevault Demo: https://dvgyl.github.io/noisevault/
SCRIPT (2026). Research collaboration on stylus-based drawing kinematics. Research collaboration on whether stylus-based drawing kinematics could inform non-diagnostic triage, with the Sensory-Motor Integration Lab (SMIL) at Rutgers University and its director, Prof. Elizabeth B. Torres. My role is research collaborator for SCRIPT.
Semantic Integrity Harness (2026). Research tooling for what LLM systems preserve. Research tooling around checking how LLM systems preserve human intentions, preferences and boundaries.
Agentic Math
The small-coefficient upper half of the Keller–Klein conjecture (2026). For normalized Rademacher sums whose coefficients are all at most 0.07 in magnitude, the AI-generated manuscript establishes the missing small-coefficient upper Berry–Esseen estimate. Combining this part with Paata Ivanisvili’s separate computer-assisted estimates would complete the conjecture. The small-coefficient theorem and its analytic ingredients are formalized in Lean. The original repository package does not formalize Ivanisvili’s separate estimates. A combined manuscript has been exchanged with Ivanisvili, but equivalence between the formal statement and the original conjecture still requires an independent check. System: autonomous AI research agents. The problem, Keller–Klein, Conjecture 9.3 (Berry–Esseen bound for Rademacher sums): https://doi.org/10.1016/j.aim.2022.108558 Write-up: https://github.com/dvgyl/math-and-theory/blob/main/papers/mathematics/keller-klein/manuscript.pdf Source and proofs: https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/keller-klein
Finite real counterexamples and spectral obstructions for q-permanent monotonicity (2026). The manuscript constructs an explicit positive-definite real matrix of order 896 whose q-permanent decreases at two rational parameters inside (0,1). It extends the construction to every order at least 896, giving a counterexample to the real-symmetric monotonicity statement. Lean checks the general endpoint identity, the certificate logic, and the reduction to rational positive-definite witnesses. The decisive large-integer inequality for the concrete matrix is verified by two independent exact programs outside Lean. Historical priority and full external review are not certified. System: autonomous AI research agents. The problem, Bapat–Lal real-symmetric q-permanent monotonicity conjecture: https://doi.org/10.1016/0024-3795(94 Write-up: https://github.com/dvgyl/math-and-theory/blob/main/papers/mathematics/q-permanent-finite/manuscript.pdf Source and proofs: https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/q-permanent-finite
Sharp stability and exact cap optima for Rademacher sums (2026). A follow-up develops sharp inverse and stability theorems for small support gaps in Rademacher sums, including an exact nonlinear modulus and extremizer classifications. It also reports exact Kolmogorov-distance cap optima on additional coefficient intervals. The structural inverse, stability and saturated-modulus statements are formalized in Lean. The Kolmogorov-distance formulas are conventional and interval-certificate-based, and conditional on external results including the completed Keller–Klein comparison. Neither the conditional conclusions nor priority have been independently certified. System: autonomous AI research agents. The problem, Extensions of the Keller–Klein Rademacher-sum programme: https://doi.org/10.1016/j.aim.2022.108558 Write-up: https://github.com/dvgyl/math-and-theory/blob/main/papers/mathematics/keller-klein-sharp-stability/manuscript.pdf Source and proofs: https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/keller-klein-sharp-stability
The exact last-gradient bound for constant-step gradient descent in the strongly convex case (2026). The manuscript derives the exact worst-case final-gradient bound for constant-step gradient descent on real Hilbert spaces, including strongly convex objectives and all normalized steps from 0 to 2. Lean covers the actual-function bound and normalized attaining examples for every horizon. Arbitrary-scale sharpness uses an ordinary rescaling proof. Historical priority and external expert review remain open. System: autonomous AI research agents. The problem, Taylor–Hendrickx–Glineur Conjecture 3: https://doi.org/10.1007/s10107-016-1009-3 Write-up: https://github.com/dvgyl/math-and-theory/blob/main/papers/mathematics/strong-gradient/manuscript.pdf Source and proofs: https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/strong-gradient
A narrow interval for the universal multiplier step of two-block ADMM (2026). The work proves convergence of the specified two-block ADMM method for multiplier steps up to 1.886795 and constructs periodic orbits above approximately 1.886884. Together these narrow the unknown universal threshold to an interval narrower than 0.00009. The stated convergence theorem, certificate reductions and periodic-orbit construction have Lean formalizations. The exact universal threshold remains open; the scalar-case result and certain consequences are conventional proofs. System: autonomous AI research agents. The problem, Glowinski’s ADMM multiplier-relaxation question: https://doi.org/10.1007/s10957-018-1338-x Write-up: https://github.com/dvgyl/math-and-theory/blob/main/papers/mathematics/admm-multiplier-step/manuscript.pdf Source and proofs: https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/admm-multiplier-step
No universal finite collapse of the upper PPT entanglement-cost hierarchy (2026). For every finite level, the manuscript constructs a full-rank Bell-diagonal state with a strictly lower value at the next level of the upper PPT entanglement-cost hierarchy. Thus no fixed finite upper level is exact for every state. Lean checks the strict hierarchy separation for the formulated semidefinite programmes. Some operational entanglement-cost consequences depend on previously published theorems, and the work does not show noncollapse in one fixed dimension. System: autonomous AI research agents. The problem, Upper PPT entanglement-cost hierarchy question after Brinster et al.: https://arxiv.org/abs/2405.09613 Write-up: https://github.com/dvgyl/math-and-theory/blob/main/papers/physics/upper-ppt-hierarchy/manuscript.pdf Source and proofs: https://github.com/dvgyl/math-and-theory/tree/main/papers/physics/upper-ppt-hierarchy
Depth-one Artin–Schreier defect towers are composita (2026). Under the specified hypotheses on a perfect henselian subfield of a Hahn field, the manuscript proves that a finite nontrivial Artin–Schreier tower has depth one exactly when it is a compositum of Artin–Schreier extensions. Both directions are formalized in Lean. The theorem is tied to the manuscript’s particular field hypotheses and definitions of depth; it is not presented as a theorem for all valued fields. System: autonomous AI research agents. The problem, Nart–Novacoski Conjecture 4.1: https://doi.org/10.1016/j.jpaa.2026.108184 Write-up: https://github.com/dvgyl/math-and-theory/blob/main/papers/mathematics/artin-schreier-depth/manuscript.pdf Source and proofs: https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/artin-schreier-depth
Matrix-pencil rank distance as an explicit completion problem (2026). The manuscript establishes an explicit equivalence between bounded rank distance of strict-equivalence classes of matrix pencils and a structured matrix-completion problem over infinite fields. The explicit dilation-and-compression equivalence is formalized in Lean. Its identification with the conjecture’s barred pencils invokes a published linearization theorem; several closely related publications were not compared in full. The conjecture-level interpretation and novelty are provisional. System: autonomous AI research agents. The problem, Dodig–Stošić bounded-rank perturbation and completion conjecture: https://doi.org/10.13001/ela.2025.9593 Write-up: https://github.com/dvgyl/math-and-theory/blob/main/papers/mathematics/matrix-pencil-completion/manuscript.pdf Source and proofs: https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/matrix-pencil-completion
Counterexamples to the Kronecker-square lower bound for nonnegative rank (2026). The work gives a rational nonnegative matrix whose Kronecker square has nonnegative rank at most 109, below the conjectured lower bound of 110, and extends the construction to an infinite family. Lean formalizes the general family and the relevant nonnegative-rank inequalities, with exact rational verification of the factorization. It does not determine the exact nonnegative rank of each Kronecker square. System: autonomous AI research agents. The problem, Vandaele–Gillis–Glineur–Tuyttens Conjecture 1: https://doi.org/10.1007/s10898-015-0350-z Write-up: https://github.com/dvgyl/math-and-theory/blob/main/papers/mathematics/nonnegative-rank-kronecker/manuscript.pdf Source and proofs: https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/nonnegative-rank-kronecker
Escaping Nesterov flows and iterates below critical damping (2026). The manuscript gives the exact universal boundedness threshold r = 3 in a specified infinite-dimensional Hilbert-space setting, with explicit escaping examples below the threshold and a corresponding discrete result. The Hilbert-space and discrete bounds and part of the planar escape analysis are formalized. The finite-dimensional interval 2 < r < 3 remains open, and some planar-range arguments use conventional proofs. System: autonomous AI research agents. The problem, Boundedness below critical damping in Nesterov acceleration: https://arxiv.org/abs/2510.23513 Write-up: https://github.com/dvgyl/math-and-theory/blob/main/papers/mathematics/nesterov-subcritical/manuscript.pdf Source and proofs: https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/nesterov-subcritical
Universal entanglement embezzlement with inverse-quadratic logarithmic infidelity (2026). The work constructs a target-independent entanglement catalyst with local dimension 2^(4L) and a root-infidelity bound of at most 125m/L² for targets having m Schmidt coefficients. The finite-complex-Hilbert-space construction and its local basis permutations are formalized; arbitrary external Schmidt-basis changes are not separately formalized. Independent novelty review remains pending. System: autonomous AI research agents. The problem, Leung–Wang question on universal entanglement-embezzling rates: https://arxiv.org/abs/1311.6842 Write-up: https://github.com/dvgyl/math-and-theory/blob/main/papers/physics/universal-embezzlement/manuscript.pdf Source and proofs: https://github.com/dvgyl/math-and-theory/tree/main/papers/physics/universal-embezzlement
i have also discovered many minor results and advances. the collection is here. https://github.com/dvgyl/math-and-theory