Recent searches

No recent searches

Search options

Only available when logged in.
sigmoid.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
A social space for people researching, working with, or just interested in AI!

Administered by:

Server stats:

574
active users

sigmoid.social: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.4.3

#ai4math

0 posts0 participants0 posts today
José A. Alonso

Solving formal math problems by decomposition and iterative reflection. Yichi Zhou et als. arxiv.org/abs/2507.15225v1 #AI4Math #LLMs #ProofAssistants #LeanProver #Math

arXiv.orgSolving Formal Math Problems by Decomposition and Iterative ReflectionGeneral-purpose Large Language Models (LLMs) have achieved remarkable success in intelligence, performing comparably to human experts on complex reasoning tasks such as coding and mathematical reasoning. However, generating formal proofs in specialized languages like Lean 4 remains a significant challenge for these models, limiting their application in complex theorem proving and automated verification. Current approaches typically require specializing models through fine-tuning on dedicated formal corpora, incurring high costs for data collection and training. In this work, we introduce \textbf{Delta Prover}, an agent-based framework that orchestrates the interaction between a general-purpose LLM and the Lean 4 proof environment. Delta Prover leverages the reflection and reasoning capabilities of general-purpose LLMs to interactively construct formal proofs in Lean 4, circumventing the need for model specialization. At its core, the agent integrates two novel, interdependent components: an algorithmic framework for reflective decomposition and iterative proof repair, and a custom Domain-Specific Language (DSL) built upon Lean 4 for streamlined subproblem management. \textbf{Delta Prover achieves a state-of-the-art 95.9\% success rate on the miniF2F-test benchmark, surpassing all existing approaches, including those requiring model specialization.} Furthermore, Delta Prover exhibits a significantly stronger test-time scaling law compared to standard Best-of-N proof strategies. Crucially, our findings demonstrate that general-purpose LLMs, when guided by an effective agentic structure, possess substantial untapped theorem-proving capabilities. This presents a computationally efficient alternative to specialized models for robust automated reasoning in formal environments.
José A. Alonso

Lean FRO and Mathlib receive $10M from XTX Markets founder Alex Gerko to further advance the use of AI for mathematical research. renaissancephilanthropy.org/ne #AI4Math #ITP #LeanProver #Math

Renaissance Philanthropy – A brighter future for all through science, technology, and innovationLean FRO and Mathlib receive $10M from XTX Markets Founder Alex Gerko to further advance the use of AI for mathematical research — Renaissance Philanthropy – A brighter future for all through science, technology, and innovationFOR IMMEDIATE RELEASE July 24, 2025 Contact: media@renphil.org ; richard.hillary@xtxmarkets.com ; pr@convergentresearch.org
TrendingLive feeds
About