Publications (12)
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…
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,…
Humanity's Last Exam
Long Phan, Alice Gatti, Ziwen Han +1144
Benchmarks are important tools for tracking the rapid advancements in large language model (LLM) capabilities. However, benchmarks are not keeping pace in difficulty: LLMs now achi…
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…
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…
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…