37 citations · 79 across the 10 of their papers we have counts for
11 papers
Advancing Mathematics Research with AI-Driven Formal Proof Search
George Tsoukalas, Anton Kovsharov, Sergey Shirobokov +18
Large language models (LLMs) increasingly excel at mathematical reasoning, but their unreliability limits their utility in mathematics research. A mitigation is using LLMs to gener…
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,…
The JPEG XL Image Coding System: History, Features, Coding Tools, Design Rationale, and Future
Jon Sneyers, Jyrki Alakuijala, Luca Versari +9
JPEG XL is a new image coding system offering state-of-the-art compression performance, lossless JPEG recompression, and advanced features. It aims to replace JPEG, PNG, GIF, and o…
AutoNumerics-Zero: Automated Discovery of State-of-the-Art Mathematical Functions
Esteban Real, Mirko Rossini, Connal de Souza +7
Transcendental functions, such as the exponential, are central to scientific computing, yet they cannot be natively calculated by digital hardware. Instead, computers must approxim…
Intelligent Matrix Exponentiation
Thomas Fischbacher, Iulia M. Comsa, Krzysztof Potempa +3
We present a novel machine learning architecture that uses the exponential of a single input-dependent matrix as its only nonlinearity. The mathematical simplicity of this architec…
Committee Draft of JPEG XL Image Coding System
Alexander Rhatushnyak, Jan Wassenberg, Jon Sneyers +15
JPEG XL is a practical approach focused on scalable web distribution and efficient compression of high-quality images. It provides various benefits compared to existing image forma…
SO(8) Supergravity and the Magic of Machine Learning
Iulia M. Comsa, Moritz Firsching, Thomas Fischbacher
Using de Wit-Nicolai supergravity as an example, we show how modern Machine Learning software libraries such as Google's TensorFlow can be employed to g…
The complete enumeration of 4-polytopes and 3-spheres with nine vertices
Moritz Firsching
We describe an algorithm to enumerate polytopes. This algorithm is then implemented to give a complete classification of combinatorial spheres of dimension 3 with 9 vertices and de…
Realizability and inscribability for simplicial polytopes via nonlinear optimization
Moritz Firsching
We show that nonlinear optimization techniques can successfully be applied to realize and to inscribe matroid polytopes and simplicial spheres. Thus we obtain a complete classifica…
Computing maximal copies of polytopes contained in a polytope
Moritz Firsching
Kepler (1619) and Croft (1980) have considered largest homothetic copies of one regular polytope contained in another regular polytope. For arbitrary pairs of polytopes we propose…
Real Equivariant Bordism for elementary abelian 2-groups
Moritz Firsching
We give a description of real equivariant bordism for elementary abelian 2-groups, which is similar to the description of complex equivariant bordism for the group S^1 x ... x S^1…