A curated map of papers I think are worth reading across AI4Math, AI4Science, world models, machine learning theory, and reinforcement learning.
DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
A major Lean 4 prover built around recursive subgoal decomposition and reinforcement learning.
PaperGoedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
Open-source prover training with synthetic formal statements and iterative proof generation.
PaperGold-Medalist Performance in Solving Olympiad Geometry with AlphaGeometry2
A strong example of language models, symbolic engines, and search combining for Olympiad geometry.
PaperDeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
Proof-assistant feedback plus tree search for Lean theorem proving.
PaperLarge Language Models as Copilots for Theorem Proving in Lean
Lean Copilot integrates LLM inference directly into Lean workflows for proof assistance.
PaperLeanDojo: Theorem Proving with Retrieval-Augmented Language Models
A benchmark and retrieval-augmented environment that helped standardize neural theorem proving in Lean.
PaperLlemma: An Open Language Model for Mathematics
A math-specialized language model line that became a useful baseline for mathematical reasoning.
PaperProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
A benchmark for natural-language-to-Lean formalization and undergraduate theorem proving.
PaperminiF2F: A Cross-System Benchmark for Formal Olympiad-Level Mathematics
A small but influential benchmark for comparing formal math systems across proof assistants.
PaperA Foundation Model for the Earth System
Aurora shows how one model can transfer across weather, air quality, waves, and other Earth-system tasks.
PaperA Generative Model for Inorganic Materials Design
MatterGen uses diffusion-style generation for controllable discovery of stable inorganic materials.
PaperOrb-v3: Atomistic Simulation at Scale
A scalable universal interatomic potential focused on accuracy, latency, memory, and larger atomistic systems.
PaperAccurate Structure Prediction of Biomolecular Interactions with AlphaFold 3
A landmark structure model for proteins, nucleic acids, small molecules, ions, and modified residues.
PaperProbabilistic Weather Forecasting with Machine Learning
GenCast is a diffusion-based ensemble weather model for calibrated medium-range forecasts.
PaperMatterSim: A Deep Learning Atomistic Model Across Elements, Temperatures and Pressures
A broadly trained atomistic model for efficient simulation and property prediction under realistic conditions.
PaperScaling Deep Learning for Materials Discovery
GNoME pushed graph-network based materials discovery to a very large design space.
PaperLearning Skillful Medium-Range Global Weather Forecasting
GraphCast is a reference point for fast, data-driven global forecasting at operational scales.
PaperTowards Foundation Models for Scientific Machine Learning
A useful paper for thinking about pretraining, transfer, and scaling for PDE-centered AI4Science.
PaperNeural Operator: Learning Maps Between Function Spaces
The conceptual base for learning operators rather than finite-dimensional vector maps.
PaperFourier Neural Operator for Parametric Partial Differential Equations
A core architecture for PDE surrogate modeling using spectral convolution.
PaperGenie: Generative Interactive Environments
A generative world model that turns internet videos into controllable interactive environments.
PaperMastering Diverse Domains through World Models
DreamerV3 is a strong general-purpose model-based RL baseline across many domains.
PaperTD-MPC2: Scalable, Robust World Models for Continuous Control
A practical world-model control stack for scalable continuous-control learning.
PaperTransformers are Sample-Efficient World Models
IRIS uses a transformer world model for sample-efficient Atari learning.
PaperMastering Atari, Go, Chess and Shogi by Planning with a Learned Model
MuZero remains one of the cleanest examples of planning with a learned model.
PaperWorld Models
The compact latent-dynamics paper that gave the area its modern name and aesthetic.
PaperSelf-Supervised Learning from Images with a Joint-Embedding Predictive Architecture
I-JEPA is a clean predictive-representation paper, useful for thinking about non-generative world modeling too.
PaperSharpness-Aware Minimization for Efficiently Improving Generalization
A clean optimization lens on flat minima and generalization.
PaperReconciling Modern Machine-Learning Practice and the Classical Bias-Variance Trade-Off
The double-descent paper that reframed overparameterized generalization.
PaperUnderstanding Deep Learning Requires Rethinking Generalization
A classic stress test for simple explanations of why deep networks generalize.
PaperRT-2: Vision-Language-Action Models Transfer Web Knowledge to Robotic Control
A key paper for grounding web-scale vision-language representations in robot actions.
PaperDecision Transformer: Reinforcement Learning via Sequence Modeling
A simple and influential framing of offline RL as conditional sequence modeling.
PaperBandit Algorithms
A precise modern treatment of bandits, regret, optimism, and exploration.
BookReinforcement Learning: An Introduction
Sutton and Barto remain the backbone reference for RL concepts.
Book