SearcharxivSearch

arXiv subjects

Oliver Nash

Publications and source records attributed to Oliver Nash.

9 recordsLinked to original sources

SPDEBench: An Extensive Benchmark for Learning Stochastic PDEs

Stochastic Partial Differential Equations (SPDEs) driven by random noise play a central role in modeling physical processes with rough spatio-temporal dynamics, such as turbulence flows, superconductors, and quantum dynamics. Although machine learning (ML)-based surrogate models have shown promise for efficiently approximating such dynamics, progress remains limited by the lack of a unified benchmark with controlled data generation and comprehensive evaluation. This gap is particularly significant for singular SPDEs, for which benchmark datasets are largely unavailable and reliable simulation requires numerically delicate schemes based on renormalization. Moreover, subtle differences in data-generation procedures, such as noise approximation, basis choice, and the inclusion of renormalization, can significantly affect the resulting datasets and, consequently, model evaluation. We introduce SPDEBench, the first unified benchmark for ML-based SPDE learning. SPDEBench provides ready-to-use datasets for physically and mathematically significant SPDEs on 1-3D domains with periodic or Dirichlet boundary condition. Both regular and singular SPDEs are taken into consideration. SPDEBench also incorporates representative ML baselines in operator learning, together with 7 evaluation metrics, including Sobolev and distributional metrics beyond the standard $L^2$-error. Supported by SPDEBench, we conduct systematic evaluations of model accuracy, robustness, and out-of-distribution generalization under controlled data variations. Our numerical results show that SPDE-aware architectures generally achieve stronger performance than generic operator-learning baselines. These findings establish SPDEBench as a reproducible and extensible resource, paving pathway for principled benchmarking and architecture design for stochastic spatio-temporal dynamics.

cs.LG

Engel's theorem in Mathlib

We discuss the theory of Lie algebras in Lean's Mathlib library. Using nilpotency as the theme, we outline a computer formalisation of Engel's theorem and an application to root space theory. We emphasise that all arguments work with coefficients in any commutative ring.

cs.LO

A formalisation of Gallagher's ergodic theorem

Gallagher's ergodic theorem is a result in metric number theory. It states that the approximation of real numbers by rational numbers obeys a striking 'all or nothing' behaviour. We discuss a formalisation of this result in the Lean theorem prover. As well as being notable in its own right, the result is a key preliminary, required for Koukoulopoulos and Maynard's stunning recent proof of the Duffin-Schaeffer conjecture.

cs.LO

Formalising the $h$-principle and sphere eversion

In differential topology and geometry, the h-principle is a property enjoyed by certain construction problems. Roughly speaking, it states that the only obstructions to the existence of a solution come from algebraic topology. We describe a formalisation in Lean of the local h-principle for first-order, open, ample partial differential relations. This is a significant result in differential topology, originally proven by Gromov in 1973 as part of his sweeping effort which greatly generalised many previous flexibility results in topology and geometry. In particular it reproves Smale's celebrated sphere eversion theorem, a visually striking and counter-intuitive construction. Our formalisation uses Theillière's implementation of convex integration from 2018. This paper is the first part of the sphere eversion project, aiming to formalise the global version of the h-principle for open and ample first order differential relations, for maps between smooth manifolds. Our current local version for vector spaces is the main ingredient of this proof, and is sufficient to prove the titular corollary of the project. From a broader perspective, the goal of this project is to show that one can formalise advanced mathematics with a strongly geometric flavour and not only algebraically-flavoured

cs.LO

Formalising Lie algebras

Lie algebras are an important class of algebras which arise throughout mathematics and physics. We report on the formalisation of Lie algebras in Lean's Mathlib library. Although basic knowledge of Lie theory will benefit the reader, none is assumed; the intention is that the overall themes will be accessible even to readers unfamiliar with Lie theory. Particular attention is paid to the construction of the classical and exceptional Lie algebras. Thanks to these constructions, it is possible to state the classification theorem for finite-dimensional semisimple Lie algebras over an algebraically closed field of characteristic zero. In addition to the focus on Lie theory, we also aim to highlight the unity of Mathlib. To this end, we include examples of achievements made possible only by leaning on several branches of the library simultaneously.

cs.LO

K-theory, LQEL manifolds and Severi varieties

We use topological K-theory to study non-singular varieties with quadratic entry locus. We thus obtain a new proof of Russo's Divisibility Property for locally quadratic entry locus manifolds. In particular we obtain a K-theoretic proof of Zak's theorem that the dimension of a Severi variety must be 2, 4, 8 or 16 and so resolve a conjecture of Atiyah and Berndt. We also show how the same methods applied to dual varieties recover the Landman parity theorem.

math.AG

On Klein's Icosahedral Solution of the Quintic

We present an exposition of the icosahedral solution of the quintic equation first described in Klein's classic work "Lectures on the icosahedron and the solution of equations of the fifth degree". Although we are heavily influenced by Klein we follow a slightly different approach which enables us to arrive at the solution more directly.

math.AG

Differential geometry of monopole moduli spaces

This thesis was motivated by a desire to understand the natural geometry of hyperbolic monopole moduli spaces. We take two approaches. Firstly we develop the twistor theory of singular hyperbolic monopoles and use it to study the geometry of their charge 1 moduli spaces. After this we introduce a new way to study the moduli spaces of both Euclidean and hyperbolic monopoles by applying Kodaira's deformation theory to the spectral curve. We obtain new results in both the Euclidean and hyperbolic cases. In particular we prove new cohomology vanishing theorems and find that the hyperbolic monopole moduli space appears to carry a new type of geometry whose complexification is similar to the complexification of hyperkähler geometry but with different reality conditions.

math.DG