From the 1 of 12 linked papers with an AI index.
12 papers
Optimal geometric barriers for weighted observability of heat semigroups on metric measure spaces
Vincent Boulard, Amaury Hayat, Emmanuel Trélat
The paper proves that the exponential small‑time factor e^{-γ/t} in weighted observability inequalities for heat equations is dictated by the geometry of the observation set, estab…
LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics
Antoine Peyronnet, Fabian Gloeckle, Amaury Hayat
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 c…
Formalizing Mathematics at Scale
Ahmad Rammal, Niket Patel, Fabian Gloeckle +5
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…
Quantitative Fredholm backstepping and rapid stabilization
Ludovick Gagnon, Amaury Hayat, Swann Marx +2
In this paper, we address the existence of Fredholm backstepping transformations for self-adjoint and skew-adjoint operators . Under suitable assumptions on the operator and…
F-equivalence for parabolic systems and applications to the stabilization of nonlinear PDE
Vincent Boulard, Amaury Hayat
We consider the -equivalence problem for parabolic systems: under which conditions a control system, governed by a parabolic operator and a control operator , can be made…
WybeCoder: Verified Imperative Code Generation
Fabian Gloeckle, Mantas Baksys, Darius Feher +5
Recent progress in large language models (LLMs) has substantially advanced automatic code generation and formal theorem proving, yet software verification has not seen comparable g…