5 papers
Tubular Neighbourhoods of Pfaffian Sets and Applications to Neural Networks
Paul Lezeau, Martin Lotz
We derive bounds for the volume of tubular neighbourhoods of smooth Pfaffian hypersurfaces, generalising known results for algebraic varieties. The bounds are given in terms of the…
SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Austin Letson, Leopoldo Sarra, Auguste Poiroux +9
We present SorryDB, a dynamically-updating benchmark of open Lean tasks drawn from 78 real world formalization projects on GitHub. Unlike existing static benchmarks, often composed…
Non-Archimedean Polydisc Spaces and Applications to Optimisation
Paul Lezeau, Yiannis Fam, Anthea Monod +1
We propose a new framework for optimisation over non-Archimedean spaces inspired by Berkovich geometry. Specifically, we introduce polydisc spaces, which consists of products of cl…
Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics
Moritz Firsching, Paul Lezeau, Salvatore Mercuri +8
As automated reasoning systems advance rapidly, there is a growing need for research-level formal mathematical problems to accurately evaluate their capabilities. To address this,…
Tropical Expressivity of Neural Networks
Paul Lezeau, Thomas Walker, Yueqi Cao +2
We propose an algebraic geometric framework to study the expressivity of linear activation neural networks. A particular quantity of neural networks that has been actively studied…