LeanMarathon uses four contract-scoped agents on an evolving blueprint coordinated by a two-stage orchestrator to formalize seven theorems from Erdős problems in Lean, proving 258 lemmas with no sorry across three runs.
hub
Early science acceleration experiments with gpt-5
15 Pith papers cite this work, alongside 2 external citations. Polarity classification is still indexing.
15
Pith papers citing it
2
external citations · external index
hub tools
citation-role summary
background 4
citation-polarity summary
years
2026 15roles
background 4polarities
background 4representative citing papers
Symmetries in next-token prediction targets induce corresponding geometric symmetries such as circulant matrices and equiangular tight frames in the optimal weights and embeddings of a layer-peeled LLM surrogate model.
An interactive AI workbench for mathematicians achieves 48% on FrontierMath Tier 4 and helped solve open problems in early tests.
A SAT-plus-LLM method discovers infinite families of doubly saturated Ramsey-good graphs, answering Grinstead and Roberts' 1982 question.
k-server-bench formulates potential-function discovery for the k-server conjecture as a code-based inequality-satisfaction task; current agents fully solve the resolved k=3 case and reduce violations on the open k=4 case.
LLMs given only research questions from 1000 arXiv CS papers recommend a narrower set of methods than the original papers, with effective model-entity diversity dropping from 1232 to 59-96 and stronger agreement among LLMs than with papers.
Smooth non-unique solutions exist for the PDE with f(0,x)=0 and positive M, while uniqueness holds for a large class of M, including a ChatGPT-suggested example.
A 72-video human-annotated benchmark shows multimodal LLMs lean on transcripts and fail to produce timestamp-accurate, length-bounded summaries of long videos.
RQGM enables co-evolution of agents and evaluators across epochs with non-stationary utilities, reporting gains in coding pass rates, paper acceptance, and proof grading over prior self-improving agents.
Introduces the Agentic Publication Protocol (APP) as a repository-based standard for publishing papers together with reproducibility artifacts and agent instructions.
Five improved inequalities were found with AI help: better Gaussian perimeter bounds for convex sets, sharper L2-L1 moments on the Hamming cube, a strengthened autoconvolution inequality, improved g-Sidon set bounds, and an optimal balanced Szarek inequality.
Develops a framework representing AI-assisted research via five operators and principles for evidence-licensed claims, distinguishing claim semantics and introducing epistemic debt.
A survey of reasoning language model adoption across 28 ERC scientific disciplines finds large maturity gaps, especially when only public resources are counted.
AI will evolve from a research tool into a collaborator, fundamentally reshaping scientific collaboration, discovery, publishing, and evaluation while requiring continuous learning and idea diversity for original contributions.
The paper introduces neural-network trial wave functions for variational Monte Carlo, frames the variational method as unsupervised learning, and illustrates the approach on the Yukawa potential and hydrogen molecule.
citing papers explorer
-
LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization
LeanMarathon uses four contract-scoped agents on an evolving blueprint coordinated by a two-stage orchestrator to formalize seven theorems from Erdős problems in Lean, proving 258 lemmas with no sorry across three runs.
-
Uncovering Symmetry Transfer in Large Language Models via Layer-Peeled Optimization
Symmetries in next-token prediction targets induce corresponding geometric symmetries such as circulant matrices and equiangular tight frames in the optimal weights and embeddings of a layer-peeled LLM surrogate model.
-
AI co-mathematician: Accelerating mathematicians with agentic AI
An interactive AI workbench for mathematicians achieves 48% on FrontierMath Tier 4 and helped solve open problems in early tests.
-
Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery
A SAT-plus-LLM method discovers infinite families of doubly saturated Ramsey-good graphs, answering Grinstead and Roberts' 1982 question.
-
$k$-server-bench: Automating Potential Discovery for the $k$-Server Conjecture
k-server-bench formulates potential-function discovery for the k-server conjecture as a code-based inequality-satisfaction task; current agents fully solve the resolved k=3 case and reduce violations on the open k=4 case.
-
Thinking Like a Scientist? A Structural Study of LLM-Generated Research Methods
LLMs given only research questions from 1000 arXiv CS papers recommend a narrower set of methods than the original papers, with effective model-entity diversity dropping from 1232 to 59-96 and stronger agreement among LLMs than with papers.
-
Non-uniqueness for a differential equation and a proof by ChatGPT
Smooth non-unique solutions exist for the PDE with f(0,x)=0 and positive M, while uniqueness holds for a large class of M, including a ChatGPT-suggested example.
-
LVSum: A Benchmark for Timestamp-Aware Long Video Summarization
A 72-video human-annotated benchmark shows multimodal LLMs lean on transcripts and fail to produce timestamp-accurate, length-bounded summaries of long videos.
-
The Red Queen G\"odel Machine: Co-Evolving Agents and Their Evaluators
RQGM enables co-evolution of agents and evaluators across epochs with non-stationary utilities, reporting gains in coding pass rates, paper acceptance, and proof grading over prior self-improving agents.
-
Agentic Publication Protocol: An Attempt to Modernize Scientific Publication
Introduces the Agentic Publication Protocol (APP) as a repository-based standard for publishing papers together with reproducibility artifacts and agent instructions.
-
Grokability in five inequalities
Five improved inequalities were found with AI help: better Gaussian perimeter bounds for convex sets, sharper L2-L1 moments on the Hamming cube, a strengthened autoconvolution inequality, improved g-Sidon set bounds, and an optimal balanced Szarek inequality.
-
The Calibration Turn in AI-Assisted Research: A Conceptual and Methodological Framework for Evidence-Licensed Claims
Develops a framework representing AI-assisted research via five operators and principles for evidence-licensed claims, distinguishing claim semantics and introducing epistemic debt.
-
Reasoning4Sciences: Bridging Reasoning Language Models to All Scientific Branches
A survey of reasoning language model adoption across 28 ERC scientific disciplines finds large maturity gaps, especially when only public resources are counted.
-
The Agentification of Scientific Research: A Physicist's Perspective
AI will evolve from a research tool into a collaborator, fundamentally reshaping scientific collaboration, discovery, publishing, and evaluation while requiring continuous learning and idea diversity for original contributions.
-
Introduction to the artificial neural network-based variational Monte Carlo method
The paper introduces neural-network trial wave functions for variational Monte Carlo, frames the variational method as unsupervised learning, and illustrates the approach on the Yukawa potential and hydrogen molecule.