Day 4: Mathematical AI, 4D world models, time series and tabular data

I have no live notes from the fourth day of the school, so this page is not a record of the talks. It is a set of topic primers, written afterwards from general knowledge, that explain the ideas each session was about. Read together, the four topics share one question: how do we build learned models whose outputs can be trusted as predictions about a system, rather than as plausible-looking text, images or numbers? Mathematical AI answers it with a perfect verifier, 4D world models with physics, time-series and tabular foundation models with broad pretraining and calibrated uncertainty, and world models with the ability to simulate the consequences of actions. In every case the interesting part is where the learned component ends and the checkable structure begins.

Talks

The Rise and Ramifications of Artificial Mathematical Intelligence — Tony Feng (UC Berkeley / Google DeepMind)

Background primer written after the school, not a record of the talk. It covers the topic, not the speaker's content.

Informal and formal mathematics

Most mathematics is written informally: proofs in natural language mixed with notation, checked by human readers who fill in routine steps. Large language models can now produce text of this kind, including multi-step arguments for competition problems. The difficulty is that a proof can read convincingly and still be wrong, and checking it takes the same expertise as writing it.

Formal mathematics removes that ambiguity. In a proof assistant (an interactive theorem prover), statements and proofs are written in a precise language, and a small trusted kernel checks every inference mechanically. Lean, in its current version Lean 4, is the most widely used system in the AI-for-math community, and Mathlib is its large, community-maintained library of formalized definitions and theorems.

The key property is that a formal proof is a certificate. If Lean accepts a proof, the theorem holds relative to the stated definitions, with no further judgment required. This converts "is the proof right?" into a program that returns yes or no. In reinforcement-learning terms it is an ideal verifiable reward: binary, cheap to compute and impossible to fool by style. This is the same setting as reinforcement learning with verifiable rewards, discussed on Day 3, in its cleanest form. An informal proof is like a lawyer's argument, persuasive to a reader; a formal proof is like a contract that a machine can audit clause by clause.

Main approaches

Several lines of work coexist, and they differ mainly in where the verifier sits.

• LLMs on informal math. Chain-of-thought reasoning on competition-style problems. Strong and broad, but not self-certifying.
• Autoformalization. Translating natural-language statements and proofs into formal code such as Lean. This is the bridge between the very large informal literature and the much smaller formal one.
• Neural theorem proving. A model proposes the next proof step (a tactic), the proof assistant checks it and returns the new goal state, and a search procedure (tree search, often trained with RL) explores alternatives when a branch fails.
• AlphaGeometry (DeepMind). A neuro-symbolic system for olympiad geometry: a language model suggests auxiliary constructions, such as an extra point or line, and a symbolic deduction engine carries out the rigorous reasoning. It is trained on synthetically generated geometry data rather than human proofs.
• AlphaProof (DeepMind). Reinforcement learning in the spirit of AlphaZero, operating on formal statements in Lean, with autoformalized problems serving as training material. It targets olympiad-level problems.

Neural theorem proving can be written as a search problem. Let $g$ be the current proof state (the remaining goals), and let a policy $\pi_\theta(\tau \mid g)$ assign probabilities to candidate tactics $\tau$. Applying $\tau$ in the proof assistant yields a new state $g' = \mathrm{step}(g, \tau)$ or an error. A proof is a sequence of tactics that reaches the state with no remaining goals, and the reward is

$$ r = \begin{cases} 1 & \text{if the kernel accepts the completed proof,} \\ 0 & \text{otherwise.} \end{cases} $$

The policy only needs to be good enough to make search tractable; correctness is guaranteed by the kernel, not by the model.

Ramifications

• Verification at scale. Machine-checked proofs could reduce the refereeing burden and catch subtle errors in long arguments.
• A changing role for mathematicians. Effort may shift from writing every step toward choosing questions, definitions and strategy, with automated tools filling in details.
• Bottlenecks. Formal libraries cover only part of mathematics, and autoformalization can silently change the meaning of a statement. A system can then prove the wrong theorem correctly, and the kernel will not notice, because it checks the proof against the statement as written.
• Relevance to science. Mathematics is the cleanest testbed for machine reasoning because the verifier is perfect. The lessons transfer naturally to code, where tests act as partial verifiers, and more loosely to scientific domains where verification is partial, noisy or expensive.

Scaling 4D World Models for Scientific AI: Balancing Physics and Data — Peter Yichen Chen (University of British Columbia)

Background primer written after the school, not a record of the talk. It covers the topic, not the speaker's content.

What "4D" means

Here 4D means three spatial dimensions plus time. A 4D model represents how a 3D scene or physical system evolves: its geometry, motion, deformation and material behavior. The goal is twofold. From observations such as images, video or sensor readings, the model should reconstruct the current state, and it should then predict or simulate future states, ideally under conditions that were never observed.

Representing 3D

There are three broad families of representation.

• Explicit representations: meshes, point clouds and voxel grids. They are easy to simulate on but hard to recover accurately from photographs.
• Neural fields (NeRF). A multilayer perceptron maps a 3D point and a viewing direction to a color and a density. Images are produced by volume rendering along camera rays, so the field can be learned from 2D photographs alone.
• 3D Gaussian splatting. The scene is a collection of 3D Gaussians, each with a position, covariance, color and opacity, rendered by fast rasterization. It is much faster to train and render than NeRF.

The NeRF rendering equation shows why 2D images are enough to supervise a 3D field. For a camera ray $\mathbf{r}(t) = \mathbf{o} + t\mathbf{d}$ with origin $\mathbf{o}$ and direction $\mathbf{d}$, the predicted pixel color is

$$ C(\mathbf{r}) = \int_{t_n}^{t_f} T(t)\,\sigma(\mathbf{r}(t))\,\mathbf{c}(\mathbf{r}(t), \mathbf{d})\,dt, \qquad T(t) = \exp\!\left(-\int_{t_n}^{t} \sigma(\mathbf{r}(s))\,ds\right), $$

where $\sigma$ is the learned density, $\mathbf{c}$ the learned color, $t_n$ and $t_f$ the near and far bounds, and $T(t)$ the transmittance, the probability that light travels from $t_n$ to $t$ without being absorbed. Because $C$ is differentiable in the network parameters, comparing it with observed pixels gives a training signal for the whole 3D field. Dynamic, or 4D, variants add a time input or a deformation field that moves the representation from one moment to the next.

Representing dynamics: physics or data

The harder part is how the scene changes. Two traditions offer complementary strengths.

Two ideas connect the columns. The first is differentiable simulation: if the simulator is written so that gradients flow through it, physical parameters can be fitted to observations by gradient descent. Let $\mathcal{S}_\phi$ be one simulator step with physical parameters $\phi$ (stiffness, friction, initial velocity), $s_0$ the initial state, $\mathcal{R}$ a differentiable renderer and $o_t$ the observed frame at time $t$. System identification then solves

$$ \min_{\phi} \; \sum_{t=1}^{T} \big\| \mathcal{R}\big(\mathcal{S}_\phi^{\,t}(s_0)\big) - o_t \big\|^2 , $$

where $\mathcal{S}_\phi^{\,t}$ denotes $t$ applications of the step. The same machinery can optimize designs or control signals instead of parameters.

The second is hybrid modeling: keep the physical structure and learn only the unknown parts, such as closure terms, material laws or residual corrections, or add physics as a loss term (as in physics-informed neural networks) or as a hard constraint (compare the constrained diffusion material from Day 2).

Balancing physics and data

Physics acts as a strong inductive bias: it restricts the hypothesis space to behaviors that respect known laws, which is what makes extrapolation possible from little data. Data fills the gaps where the equations are unknown, incomplete or too expensive to solve. Scaling such systems is therefore less about making one component larger and more about deciding which parts to hard-code and which to learn as the amount of data grows. Robotics, materials, fluids and biomechanics all need models that are both visually faithful and physically correct, usually from limited and noisy observations, which is exactly where this balance matters.

Reasoning / Time series / Tabular Data — Bernie Wang (MIT)

Background primer written after the school, not a record of the talk. It covers the topic, not the speaker's content.

Time series forecasting

Given a history $y_{1:t}$ and, optionally, covariates, the forecasting task is to predict the future values $y_{t+1:t+H}$ over a horizon $H$. In most applications the forecast should be probabilistic: a distribution or a set of quantiles rather than a single number, because decisions such as stocking inventory, scheduling an instrument or sizing a power reserve depend on how uncertain the future is.

A standard way to train and evaluate quantile forecasts is the quantile (pinball) loss. For a quantile level $q \in (0, 1)$, a true value $y$ and a predicted quantile $\hat{y}_q$,

$$ \rho_q(y, \hat{y}_q) = \max\big( q\,(y - \hat{y}_q),\; (q - 1)\,(y - \hat{y}_q) \big). $$

Under-prediction is penalized with weight $q$ and over-prediction with weight $1 - q$, so the minimizer of the expected loss is exactly the $q$-th quantile of the predictive distribution. Averaging $\rho_q$ over several levels gives a proper score for the whole forecast distribution.

Classical baselines such as ARIMA and exponential smoothing remain strong, especially on short, regular series. Deep models include DeepAR, an autoregressive recurrent network with a probabilistic output, and a range of transformer forecasters. Traditionally, each of these is fitted to one dataset.

Time series foundation models

The foundation-model idea is to pretrain one model on many diverse series and then forecast new series zero-shot, without per-task training. Chronos makes the analogy with language models literal: it scales each series, quantizes the scaled values into a fixed set of bins that act as tokens, and trains a T5-style language-model architecture with cross-entropy, so that forecasting becomes next-token prediction and sampling yields probabilistic forecasts. Other well-known examples are TimesFM, Moirai and Lag-Llama, which make different choices about input representation and output distribution.

Several issues remain open: series from different domains have very different frequencies and scales, covariates are hard to incorporate in a general way, and evaluation can leak information when benchmark series overlap with pretraining data.

Tabular data

Tables are the other workhorse format of science: rows are samples, columns are heterogeneous features (numeric, categorical, often with missing values). Gradient-boosted trees, as implemented in XGBoost, LightGBM and CatBoost, have long been the strong default, and deep networks often struggled to beat them.

TabPFN takes a different route. It is a transformer pretrained on synthetic datasets sampled from a prior over data-generating processes, for example random causal models. At test time the entire training table is passed as context, and the model predicts the test rows in a single forward pass. No gradient steps are taken on the new dataset; this is in-context learning. The training objective makes the network approximate the Bayesian posterior predictive distribution

$$ p(y \mid x, \mathcal{D}) = \int p(y \mid x, \phi)\, p(\phi \mid \mathcal{D})\, d\phi , $$

where $\mathcal{D}$ is the training table, $x$ a test row, $y$ its label and $\phi$ the latent data-generating process drawn from the prior. The approach is best suited to small and medium-sized tables, where the full table fits in context. A useful picture is a student who has solved millions of practice problems from a textbook generator: faced with a new table, it does not train, it recognizes the pattern.

Where reasoning comes in

Language models can read time series and tables serialized as text, but numbers in text are a poor fit: tokenization fragments digits, precision is lost, and long histories exhaust the context. A common pattern is therefore for the language model to reason about the problem and call tools, such as code, specialized forecasters or TabPFN-like models, rather than doing the arithmetic itself. Since much scientific data consists of sensor time series or tables of experiments, foundation models for these modalities promise good results on small datasets without per-task training.

World Models — Jiajun Wu (Stanford University)

Background primer written after the school, not a record of the talk. It covers the topic, not the speaker's content.

What is a world model?

A world model is a learned model of how the world evolves: given the current state, or observations of it, and an action, it predicts what happens next. Its main use is planning by imagination, trying out actions inside the model before committing to them in the real world. It is the agent's mental simulator, much as a person imagines where a ball will land before moving to catch it.

In its simplest form the model is a transition distribution $p(s_{t+1} \mid s_t, a_t)$ over the next state $s_{t+1}$ given the state $s_t$ and action $a_t$. Because raw observations such as images are high-dimensional, most modern world models work in a learned latent space. An encoder maps the observation $o_t$ to a latent state $z_t$, and the model learns

$$ z_{t+1} \sim p_\theta(z_{t+1} \mid z_t, a_t), \qquad \hat{o}_{t+1} \sim p_\theta(o_{t+1} \mid z_{t+1}), \qquad \hat{r}_{t+1} = f_\theta(z_{t+1}), $$

where $\theta$ denotes the model parameters, $\hat{o}_{t+1}$ a predicted observation and $\hat{r}_{t+1}$ a predicted reward. Planning then means rolling this transition forward for candidate action sequences and choosing actions that lead to high predicted reward, all without touching the real environment.

Key lines of work

• "World Models" (Ha & Schmidhuber). A variational autoencoder compresses frames into latents, a recurrent network predicts the next latent, and a small controller chooses actions. The agent can be trained inside its own "dream" and then deployed in the real environment.
• Dreamer (Hafner et al.). Learns latent dynamics from experience and learns behavior through imagined rollouts in latent space, a model-based reinforcement learning approach.
• MuZero. Learns a model used for planning with tree search without being given the rules of the environment. Its model only needs to predict quantities relevant to planning, such as rewards and values, not full observations.
• Video prediction and generative video models as world simulators. These generate future frames, optionally conditioned on actions. Genie, for instance, produces action-controllable generated environments.
• Structured and physical world models. These represent objects, 3D geometry and physics explicitly, linking directly to the 4D world models topic above and to physical scene understanding discussed on Day 3.

Pixels or structure

The design space has two poles. Pixel and video models scale well with data and produce realistic output, but they can be physically inconsistent: objects appear or vanish, and quantities that should be conserved are not. Structured models that reason over objects, 3D geometry and physics generalize better and are interpretable, but they are harder to learn from raw data. Much current work mixes the two, for example by using a learned perceptual front end with a structured or physics-aware dynamics core.

Why it matters for science

Science is largely about counterfactuals: what happens if we change a parameter, apply a perturbation or run a different experiment? A world model is precisely a tool for answering such questions, which connects it with the Large Physics Models material from Day 1. This also sets the evaluation bar. For a scientific world model the question is not whether its rollouts look right but whether it predicts correctly under interventions it was not trained on.

Key takeaways

Topic-level takeaways from the primers above, not from the talks.

• Formal verification in Lean turns mathematical correctness into a programmatic verifier, making mathematics the cleanest testbed for RL-style reasoning, as in AlphaProof, AlphaGeometry and autoformalization research. The remaining weak point is whether a formal statement means what the informal one intended.
• 4D world models combine 3D representations such as NeRF and Gaussian splatting with dynamics; the central design choice is how much physics to hard-code and how much to learn from data.
• Differentiable simulation and rendering let physical parameters be fitted directly to images and video by gradient descent, turning simulators into learnable components.
• Foundation models for time series (Chronos, TimesFM, Moirai, Lag-Llama) and for tables (TabPFN) bring zero-shot and in-context prediction to modalities long dominated by per-dataset models, with probabilistic outputs as a first-class requirement.
• World models (Ha & Schmidhuber, Dreamer, MuZero, Genie and generative video) are learned simulators for planning. For science, the standard is correct predictions under interventions, not visual realism.
• Across all four topics, trust comes from structure outside the network: a proof kernel, physical laws, a calibrated loss or an interventional test.

Open questions

• How reliable is autoformalization, and how can one check that a formal statement means what the informal one says?
• What benchmarks test scientific world models for physical correctness under interventions, rather than visual plausibility?
• How should time-series and tabular foundation models be evaluated when pretraining corpora may overlap with benchmark data?
• I would like to revisit the slides or recordings, if they are published, to replace these primers with the speakers' actual content.

These are my own notes and may contain errors. Not official course material. Source on GitHub.