49 citations · 86 across the 9 of their papers we have counts for
10 papers
LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
Po-Nien Kung, Linfeng Song, Dawsen Hwang +10
Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate mechanically verifiable proofs in formal languages like Lean. We present LEAP,…
Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilities
Gheorghe Comanici, Eric Bieber, Mike Schaekermann +3431
In this report, we introduce the Gemini 2.X model family: Gemini 2.5 Pro and Gemini 2.5 Flash, as well as our earlier Gemini 2.0 Flash and Flash-Lite models. Gemini 2.5 Pro is our…
MizAR 60 for Mizar 50
Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel +6
As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60\% of the Mizar theorems in the hammer setting. We also automatically pr…
Machine Learning Meets The Herbrand Universe
Jelle Piepenbrock, Josef Urban, Konstantin Korovin +3
The appearance of strong CDCL-based propositional (SAT) solvers has greatly advanced several areas of automated reasoning (AR). One of the directions in AR is thus to apply SAT sol…
The Isabelle ENIGMA
Zarathustra A. Goertzel, Jan Jakubův, Cezary Kaliszyk +3
We significantly improve the performance of the E automated theorem prover on the Isabelle Sledgehammer problems by combining learning and theorem proving in several ways. In parti…
Maximal non-compactness of Sobolev embeddings
Jan Lang, Vít Musil, Miroslav Olšák +1
It has been known that sharp Sobolev embeddings into weak Lebesgue spaces are non-compact but the question of whether the measure of non-compactness of such an embedding equals to…
Local loop lemma
Miroslav Olšák
We prove that an idempotent operation generates a loop from a strongly connected digraph containing directed cycles of all lengths under very mild (local) algebraic assumptions. Us…
Loop conditions with strongly connected graphs
Miroslav Olšák
We prove that the existence of a term satisfying in a general algebraic structure is equivalent to an existence of a term satisfying $t(x,x,y,y,z,…
Loop conditions
Miroslav Olšák
We discuss such Maltsev conditions that consist of just one linear equation, we call them loop conditions. To every such condition can be assigned a graph. We provide a classificat…
The weakest nontrivial idempotent equations
Miroslav Olšák
An equational condition is a set of equations in an algebraic language, and an algebraic structure satisfies such a condition if it possesses terms that meet the required equations…