arXiv subjects

Amaury Hayat

Publications and source records attributed to Amaury Hayat.

At least 19 recordsLinked to original sources

arXiv2026

Double-wells in a strong magnetic field: absence of tunneling for infinitely many values of the coupling constant

We prove the fixed-potential conjecture of Fefferman, Shapiro, and Weinstein for inversion-symmetric magnetic double wells. We construct a number $L_0>0$ and one smooth, compactly supported, nonpositive, nonradial single-well potential $v$, independent of both the coupling parameter $λ$ and the well displacement, such that for every fixed $L\ge L_0$ the associated magnetic double-well Hamiltonian has infinitely many exact degeneracies of its two lowest eigenvalues as $λ\to\infty$. The magnetic hopping coefficient also vanishes along an infinite sequence tending to infinity. The potential consists of a radial core and two small, reflection-related perturbations supported on one-sided quadratic cusps. Their log-flat profiles isolate two dominant hopping contributions, which we evaluate by steepest descent after inserting the radial ground-state asymptotics. The resulting asymptotic cosine expression, together with error bounds for the even--odd splitting, yields infinitely many exact eigenvalue crossings and changes of ground-state parity.

math.AP↗

arXiv2026

Optimal geometric barriers for weighted observability of heat semigroups on metric measure spaces

Weighted integrated observability inequalities for heat equations usually involve a small-time factor of the form $e^{-γ/t}$. We prove that this scale is not an artefact of Carleman or spectral methods: it is forced by the geometry of the observation set. Let $A$ be a nonnegative self-adjoint operator on sections of a finite-rank Euclidean vector bundle over a doubling metric measure space, satisfying ultracontractivity, Davies-Gaffney estimates (equivalently, finite speed of propagation for the wave equation) and a pointwise local Weyl law. If a weighted integrated observability inequality holds on a measurable set $ω$, for a fixed horizon $T\in(0,+\infty]$ and an admissible weight $h$, then, for every $0<κ<\frac{1}{2}$, $$ h(t)\leq A_{T,κ}\exp\left(-κ\frac{\mathcal{L}(ω)^2}{t}\right),\qquad 0<t<T, $$ where $\mathcal{L}(ω)$ is the essential maximal distance to $ω$, replaced by any finite radius when $\mathcal{L}(ω)=+\infty$. Thus, for $h(t)=e^{-γ/t}$, necessarily $γ\geq\mathcal{L}(ω)^2/2$. This settles, with the optimal threshold, the maximal-distance lower bound for the infinite-time constant left open in earlier work. In the control-norm convention, the fast-control rate is at least $\mathcal{L}(ω)^2/4$, recovering Miller's bound. The proof rests on the spectral packet $(\cosh(r\sqrt A)-1)e^{-tA}$. A pointwise Weyl law gives its sharp lower growth, while finite propagation speed and a weak-kernel Kannai transmutation formula make it exponentially small on $ω$. Without kernel continuity or compact resolvent, we develop pointwise spectral measures and weak wave kernels. The framework covers Laplace-type operators on compact Riemannian manifolds, coupled heat systems, Schrödinger operators on $\mathbb{R}^d$, equiregular sub-Laplacians and Grushin models, and $δ'$-coupled Laplacians on metric graphs.

math.AP↗

arXiv2026

LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics

We present a new approach for benchmarking Large Language Model (LLM) capabilities on research-level mathematics. Existing benchmarks largely rely on static, hand-curated sets of contest or textbook-style problems as proxies for mathematical research. Instead, we establish an updatable benchmark evaluating models directly on the latest research results in mathematics. This consists of an automatic pipeline that extracts lemmas from arXiv and rewrites them into self-contained statements by making all assumptions and required definitions explicit. It results in a benchmark that can be updated regularly with new problems taken directly from human mathematical research, while previous instances can be used for training without compromising future evaluations. We benchmark current state-of-the-art LLMs, which obtain around 10-15$\%$ accuracy in theorem proving (pass@1) depending on the model, showing that there is currently a large margin of progression for LLMs to reach human-level proving capabilities in a research context.

cs.AI↗

arXiv2026

Formalizing Mathematics at Scale

We present AutoformBot, a multi-agent system for building an Autoformalized Textbook Library At Scale (Atlas) in Lean 4. AutoformBot orchestrates thousands of LLM agents, equipped with formal verification tools, dependency-aware task scheduling, and collaborative version control, to translate informal textbook prose into machine-checked definitions and proofs. We apply our methods to a corpus of 26 open-access textbooks spanning analysis, algebra, topology, combinatorics, and probability, producing Atlas: a verified library of over 45,000 Lean 4 declarations and 500 thousand lines of code. We release two artifacts: (i) AutoformBot, the open-source multi-agent framework; and (ii) Atlas, the resulting formal library. Our results suggest that autoformalizing the core content of graduate-level mathematics at scale is now economically and technically feasible. This opens the door to the automated verification of both human- and machine-generated mathematics at a research level.

cs.AI↗

arXiv2026

Quantitative Fredholm backstepping and rapid stabilization

In this paper, we address the existence of Fredholm backstepping transformations for self-adjoint and skew-adjoint operators $A$. Under suitable assumptions on the operator $A$ and the possibly unbounded control operator $B$, we prove the existence of a Fredholm backstepping transformation for operators of order strictly greater than $1$. This work overcomes two major limitations of the classical Fredholm backstepping framework. One of the main contributions is the explicit identification of the underlying isomorphism used in the construction of the transformation $T$, thereby bypassing the compactness arguments and Riesz basis mechanisms traditionally used in the literature. This explicit structure enables us to derive quantitative and sharp estimates for $\|T\|_{\mathcal{L}(H;H)}$ and $\|T^{-1}\|_{\mathcal{L}(H;H)}$ with respect to the decay rate $λ$. As a consequence, we obtain quantitative rapid stabilization and small-time null controllability results for a broad class of operators.

math.OC↗

arXiv2026

F-equivalence for parabolic systems and applications to the stabilization of nonlinear PDE

We consider the $F$-equivalence problem for parabolic systems: under which conditions a control system, governed by a parabolic operator $A$ and a control operator $B$, can be made equivalent to an exponentially stable system with arbitrarily large decay rate through an appropriate control feedback law? While this problem has been resolved for finite-dimensional systems fifty years ago, good conditions for infinite-dimensional systems remain a challenge, especially for systems in spatial dimension larger than one. Our main result establishes optimal conditions for the existence of an $F$-equivalence pair $(T,K)$ for a given parabolic control system $(A,B)$. We introduce an extended framework for $F$-equivalence of parabolic operators, addressing key limitations of existing approaches, and we prove that the pair $(T,K)$ is unique if and only if $(A,B)$ is approximately controllable. As a consequence, this provides a method to construct feedback operators for the rapid stabilization of semilinear parabolic systems, possibly multi-dimensional in space. We provide several illustrative examples, including the rapid stabilization of the heat equation, the Kuramoto-Sivashinsky equation, the Navier-Stokes equations and the quasilinear heat equation.

math.AP↗

arXiv2026

WybeCoder: Verified Imperative Code Generation

Recent progress in large language models (LLMs) has substantially advanced automatic code generation and formal theorem proving, yet software verification has not seen comparable gains. To address this gap, we propose WybeCoder, an agentic code verification framework that enables prove-as-you-generate development, in which code, invariants, and proofs co-evolve. WybeCoder builds on a recent framework that combines automatic verification condition generation and SMT solving with interactive proofs in Lean. To enable systematic evaluation, we translate two benchmarks for functional verification in Lean, Verina and Clever, into equivalent imperative code specifications. On complex algorithms such as Heapsort, we observe consistent performance improvements as we scale our approach, synthesizing dozens of valid invariants and dispatching dozens of subgoals, ultimately producing hundreds of lines of verified code and overcoming plateaus reported in previous work. Our best system solves 74% of Verina tasks and 62% of Clever tasks at moderate compute budgets, substantially surpassing previous evaluations and paving the way for the automated construction of large-scale datasets of verified imperative code.

cs.SE↗

arXiv2026

Global boundary stabilization of 1d systems of scalar conservation laws

We study a system of several one-dimensional scalar conservation laws coupled through boundary feedback conditions that combine physical boundary constraints with static feedback control laws. Our first contribution establishes the well-posedness of the system in the space of $L^{\infty}$ entropy solutions. Our second contribution provides a set of sufficient dissipative conditions on the boundary coupling that ensure global exponential stability in the $L^1$ and $L^\infty$ norms.

math.AP↗

arXiv2026

Automatic Textbook Formalization

We present a case study where an automatic AI system formalizes a textbook with more than 500 pages of graduate-level algebraic combinatorics to Lean. The resulting formalization represents a new milestone in textbook formalization scale and proficiency, moving from early results in undergraduate topology and restructuring of existing library content to a full standalone formalization of a graduate textbook. The formalization comprises 130K lines of code and 5900 Lean declarations and was conducted within one week by a total of 30K Claude 4.5 Opus agents collaborating in parallel on a shared code base via version control, simultaneously setting a record in multi-agent software engineering with usable results. The inference cost matches or undercuts what we estimate as the salaries required for a team of human experts, and we expect there is still the potential for large efficiencies to be made without the need for better models. We make our code, the resulting Lean code base and a side-by-side blueprint website available open-source.

cs.AI↗

arXiv2026

Exponential stability of the linearized viscous Saint-Venant equations using a quadratic Lyapunov function

In this work, we investigate the exponential stability of the viscous Saint-Venant equations by adding to the standard hyperbolic Saint-Venant equations a viscosity term coming from the higher order approximation of the Saint-Venant equations from Navier-Stokes equations. The inclusion of viscosity transforms these equations into more complex second-order partial differential equations, accurately modeling the behavior of real-world fluids that inherently possess viscosity. We construct an explicit quadratic Lyapunov function and demonstrate that it must be diagonal in physical coordinates, revealing that certain quadratic Lyapunov functions effective in non-viscous cases become inadequate when viscosity is introduced. We find explicit sufficient conditions on the parameters of the boundary conditions such that for small viscosities a quadratic Lyapunov function exists. This result ensures the exponential stability of the linearized system around the steady-state solutions in the $L^2$ norm.

math.AP↗

arXiv2026

Boundary stabilization of flows in networks of open channels modeled by Saint-Venant equations

This work investigates the boundary stabilization of flows in star-shaped and tree-shaped networks of open channels governed by the Saint-Venant equations with a friction term. Due to the existence of the friction term, the steady-states are non-uniform. We show that any such network can be stabilized with only controls at the terminal nodes of the network, even when there are no controls at the nodes inside the network. The number of control is optimal. The main tool we use is the Lyapunov approach, and the main challenge is that the state-of-the-art Lyapunov functions developed for Saint-Venant equations with source terms cannot be used. In this work, we manage to construct a new efficient and explicit Lyapunov function and, in turn, we give explicit ranges of the control tuning parameters that depend only on the values of the given non-uniform steady-states at the ends of the branches. Moreover, this Lyapunov function also improves the existing conditions found in the last decade for a single channel modelled by Saint-Venant equations.

math.OC↗

arXiv2026

Rapid stabilization of general linear systems with F-equivalence

We study the rapid stabilization of general linear systems, when the differential operator $\mathcal{A}$ has a Riesz basis of eigenvectors. We find simple sufficient conditions for the rapid stabilization and the construction of a relatively explicit feedback operator. We use an $F$-equivalence approach \textcolor{black}{relying on Fredholm transformation} to show a stronger result: under these sufficient conditions the system is equivalent to a simple exponentially stable system, with arbitrarily large decay rate. In particular, our conditions improve the existing conditions of rapid stabilization for non-parabolic operators such as skew-adjoint systems.

math.AP↗

arXiv2026

Traffic Flow Reconstruction from Limited Collected Data

We propose an efficient method for reconstructing traffic density with low penetration rate of probe vehicles. Specifically, we rely on measuring only the initial and final positions of a small number of cars which are generated using microscopic dynamical systems. We then implement a machine learning algorithm from scratch to reconstruct the approximate traffic density. This approach leverages learning techniques to improve the accuracy of density reconstruction despite constraints in available data. For the sake of consistency, we will prove that, if only using data from dynamical systems, the approximate density predicted by our learned-based model converges to a well-known macroscopic traffic flow model when the number of vehicles approaches infinity.

math.DS↗

arXiv2024

Global Lyapunov functions: a long-standing open problem in mathematics, with symbolic transformers

Despite their spectacular progress, language models still struggle on complex reasoning tasks, such as advanced mathematics. We consider a long-standing open problem in mathematics: discovering a Lyapunov function that ensures the global stability of a dynamical system. This problem has no known general solution, and algorithmic solvers only exist for some small polynomial systems. We propose a new method for generating synthetic training samples from random solutions, and show that sequence-to-sequence transformers trained on such datasets perform better than algorithmic solvers and humans on polynomial systems, and can discover new Lyapunov functions for non-polynomial systems.

cs.LG↗

arXiv2024

Fredholm backstepping for critical operators and application to rapid stabilization for the linearized water waves

Fredholm-type backstepping transformation, introduced by Coron and Lü, has become a powerful tool for rapid stabilization with fast development over the last decade. Its strength lies in its systematic approach, allowing to deduce rapid stabilization from approximate controllability. But limitations with the current approach exist for operators of the form $|D_x|^α$ for $α\in (1,3/2]$. We present here a new compactness/duality method which hinges on Fredholm's alternative to overcome the $α=3/2$ threshold. More precisely, the compactness/duality method allows to prove the existence of a Riesz basis for the backstepping transformation for skew-adjoint operator verifying $α>1$, a key step in the construction of the Fredholm backstepping transformation, where the usual methods only work for $α>3/2$. The illustration of this new method is shown on the rapid stabilization of the linearized capillary-gravity water wave equation exhibiting an operator of critical order $α=3/2$.

math.AP↗

arXiv2024

Traffic Control via Connected and Automated Vehicles: An Open-Road Field Experiment with 100 CAVs

The CIRCLES project aims to reduce instabilities in traffic flow, which are naturally occurring phenomena due to human driving behavior. These "phantom jams" or "stop-and-go waves,"are a significant source of wasted energy. Toward this goal, the CIRCLES project designed a control system referred to as the MegaController by the CIRCLES team, that could be deployed in real traffic. Our field experiment leveraged a heterogeneous fleet of 100 longitudinally-controlled vehicles as Lagrangian traffic actuators, each of which ran a controller with the architecture described in this paper. The MegaController is a hierarchical control architecture, which consists of two main layers. The upper layer is called Speed Planner, and is a centralized optimal control algorithm. It assigns speed targets to the vehicles, conveyed through the LTE cellular network. The lower layer is a control layer, running on each vehicle. It performs local actuation by overriding the stock adaptive cruise controller, using the stock on-board sensors. The Speed Planner ingests live data feeds provided by third parties, as well as data from our own control vehicles, and uses both to perform the speed assignment. The architecture of the speed planner allows for modular use of standard control techniques, such as optimal control, model predictive control, kernel methods and others, including Deep RL, model predictive control and explicit controllers. Depending on the vehicle architecture, all onboard sensing data can be accessed by the local controllers, or only some. Control inputs vary across different automakers, with inputs ranging from torque or acceleration requests for some cars, and electronic selection of ACC set points in others. The proposed architecture allows for the combination of all possible settings proposed above. Most configurations were tested throughout the ramp up to the MegaVandertest.

eess.SY↗

arXiv2023

Traffic smoothing using explicit local controllers

The dissipation of stop-and-go waves attracted recent attention as a traffic management problem, which can be efficiently addressed by automated driving. As part of the 100 automated vehicles experiment named MegaVanderTest, feedback controls were used to induce strong dissipation via velocity smoothing. More precisely, a single vehicle driving differently in one of the four lanes of I-24 in the Nashville area was able to regularize the velocity profile by reducing oscillations in time and velocity differences among vehicles. Quantitative measures of this effect were possible due to the innovative I-24 MOTION system capable of monitoring the traffic conditions for all vehicles on the roadway. This paper presents the control design, the technological aspects involved in its deployment, and, finally, the results achieved by the experiment.

eess.SY↗

arXiv2023

Reinforcement Learning in Control Theory: A New Approach to Mathematical Problem Solving

One of the central questions in control theory is achieving stability through feedback control. This paper introduces a novel approach that combines Reinforcement Learning (RL) with mathematical analysis to address this challenge, with a specific focus on the Sterile Insect Technique (SIT) system. The objective is to find a feedback control that stabilizes the mosquito population model. Despite the mathematical complexities and the absence of known solutions for this specific problem, our RL approach identifies a candidate solution for an explicit stabilizing control. This study underscores the synergy between AI and mathematics, opening new avenues for tackling intricate mathematical problems.

math.OC↗