Supervisor: Dr. Kangning Huang, Department of Environmental Studies, New York University Shanghai

Project Overview

This project investigates why some urban neighborhoods in China thrive while others stagnate despite similar infrastructure investments. Using nonlinear dynamics and tipping point theory, students will analyze spatial bifurcation and temporal transitions in urban vitality across Chinese cities through spatial analysis, satellite image processing, and dynamical systems modeling.

---

China's rapid urbanization presents a natural laboratory for studying nonlinear urban dynamics. This research addresses critical transitions in neighborhood development through three aims:

1. Mapping spatial heterogeneity using cellular signal data, POI density, and accessibility metrics across nested spatial units;
2. Developing dynamical models incorporating feedback loops between accessibility, amenity density, and social expectations to recreate historical development patterns;
3. Identifying policy intervention points where targeted investments can tip struggling urban neighborhoods toward self-sustaining growth. Students will work with large-scale urban datasets, apply bifurcation theory to real-world systems, and develop computational models to understand when and why urban areas experience regime shifts.

Project Keywords: urban dynamics, critical transitions, bifurcation theory, Chinese urbanization, complex systems, GIS analysis, mathematical modeling, tipping points, urban, vitality, spatial heterogeneity

Supervisor: Dr. Chao Qin, College of Mathematical Sciences, Harbin Engineering University

Project Overview

This project outlines a large-scale, multi-prime computational test of the Ellenberg-Jain-Venkatesh (EJV) conjecture.1 The project will compute the statistical distribution of $p$-adic $\lambda$-invariants for $p \in \{3, 5, 7\}$ over a massive dataset of imaginary quadratic fields (discriminant $D < 10^8$). The primary goal is to resolve a statistical discrepancy observed in the foundational work 1 and to provide the first large-scale test of this conjecture.

---

The EJV conjecture is an asymptotic prediction. The discrepancy observed in their paper is statistically inconclusive due to the relatively small dataset ($D < 10^5$). This anomaly could be a small-data artifact that vanishes as $D \to \infty$, or it could be a deep, undiscovered arithmetic phenomenon—a "bias" not accounted for by the random matrix model.

To resolve this, a much larger and broader test is required.

Phase 1: Algorithmic Optimization: The existing Sage script will be re-engineered for high-performance computing. The primary bottleneck, the computation of generalized Bernoulli numbers $B_{k,\chi}$, will be heavily parallelized and optimized for large-scale cluster computation.

Phase 2: Data Generation: The optimized script will be executed for all admissible imaginary quadratic fields with discriminants $D < 10^8$ for the prime $p=3$. This massively larger dataset will allow for a definitive test of the asymptotic prediction. This computationally intensive process will then be repeated for $p=5$ and $p=7$.

Phase 3: Statistical Analysis: For each prime $p$, the observed distribution of $\lambda$-invariants will be compared against the EJV prediction $P(r) = p^{-r}\prod_{t>r}(1-p^{-t})$. This analysis will definitively answer:

1. Does the $\lambda=0$ discrepancy for $p=3$ vanish as $D \to 10^8$?
2. Do similar discrepancies appear for $p=5$ and $p=7$, and if so, do they follow a predictable pattern?

Project Keywords: Dimensionality Reduction, Computational Chemistry, Information Theory, Graph Theory, Latent Representations

Supervisor: Dr. Manuel Rissel, Institute of Mathematical Sciences, ShanghaiTech University

Project Overview

This project explores challenging control problems for simplified mathematical models describing fluids driven by localized external forces (controls). Undergraduate researchers will investigate under what assumptions there exist control forces that make the considered fluids behave like arbitrarily prescribed reference flows. This will involve the analysis of nonlinear ordinary differential equations and techniques from geometric control theory.

---

The desire to understand and control the behavior of fluid flows has been a recurring theme in the history of science. During recent centuries, such efforts culminated in  well-established mathematical descriptions of fluid flows based on nonlinear partial differential equations; for instance, the Navier-Stokes equations. To make this project accessible to undergraduate students, attention is paid to finite-dimensional approximations of the Navier-Stokes equations.

The aim of this project is to investigate the question whether frequency localized external forces can be chosen such that correspondingly forced fluids approximate arbitrarily prescribed reference flows. Hereto, the difference between two fluid trajectories will be measured in a metric which is insensitive to bounded high-frequency oscillations. This question touches topics of ongoing research, including applications to the mixing of passive particles in controlled fluid flows; however, the here considered simplified setting has its own merits.

Undergraduate researchers will explore, among others, methods from the analysis of nonlinear ordinary differential equations and techniques from geometric control theory.

---

For this project, students should have successfully completed a series of typical undergraduate mathematical analysis courses and possess some knowledge on nonlinear ordinary differential equations. Functional analysis or PDE background would be a big plus but is not necessary.

Project Keywords: fluid dynamics, nonlinear differential equations, mathematical analysis, trajectory tracking, controllability

Supervisor: Dr. Tianyu Wang, Shanghai Center for Mathematical Sciences, Fudan University

Project Overview

The rise of large language models (LLMs) has ignited progress in AI for formal mathematics, as seen in systems that interact with proof assistants like Lean. However, treating proof code as plain text fails to leverage the fundamental structure of formal reasoning — its hierarchical syntax, rigorous type systems, and stateful proof dynamics. In this project, we will explore new schemes for processing the formal mathematical languages such as Lean.

---

This project seeks to redefine the architecture of AI systems for formal mathematics. While large language models have shown promise in automating tasks in proof assistants like Lean, their core design treats mathematical reasoning as a sequence modeling problem, ignoring the rich, structured semantics of type theory and tactical proof. We propose to move beyond this paradigm by developing a new class of neural architectures that are structurally aligned with the domain of formal proof. Our research will explore models that natively represent and manipulate the abstract syntax trees, scoping rules, and dynamic proof states of languages like Lean. By explicitly encoding these structural inductive biases, we aim to build systems that learn the principles of deduction, not just the patterns of proof text. This will enable more sample-efficient learning, more reliable generalization, and a fundamentally deeper class of AI mathematical assistants, ultimately bridging the gap between statistical pattern matching and genuine formal reasoning.

Project Keywords: Math for AI, Large Language Models