An LLM-based agent with Lean verification autonomously solved multiple open Erdős problems and OEIS conjectures in the first large-scale test.
Formal mathematical reasoning: A new frontier in ai.arXiv preprint 2412.16075
9 Pith papers cite this work. Polarity classification is still indexing.
9
Pith papers citing it
citation-role summary
background 3
citation-polarity summary
roles
background 3polarities
background 3representative citing papers
FISolver trains a compact LLM on backward-generated (differential equation, first integral) pairs and uses guided reinforcement learning to outperform larger models and Mathematica on first-integral benchmarks at lower cost.
Lean Atlas visualizes Lean 4 dependency graphs and applies Lean Compass to reduce the nodes needing human semantic review by 27-99% across six evaluated projects.
AlphaEvolve is an LLM-orchestrated evolutionary coding agent that discovered a 4x4 complex matrix multiplication algorithm using 48 scalar multiplications, the first improvement over Strassen's algorithm in 56 years, plus optimizations for Google data centers and hardware.
Tri-RAG turns external knowledge into Condition-Proof-Conclusion triplets and retrieves via the Condition anchor to improve efficiency and quality in LLM RAG.
Introduces a conceptual framework for curiosity-driven reward-based learning in audio via continuous search for novel sound sources, with an overview of prior work and a proof-of-concept.
Proposes a three-layer framework using formal AI reasoning for verification, derivation, and discovery in wireless communications theory.
An integrated survey organizing AI mathematical reasoning into informal, formal, discovery, and technique axes while cataloging benchmarks and assessing failure modes.