Bin Dong(董彬) Long CV, Short CV
Professor
Beijing International Center for Mathematical
Research (BICMR),
Center for Machine Learning Research (CMLR)
Office: BICMR，77101; Phone:
+8610-62744091
Email: dongbin {at} math {dot} pku {dot} edu {dot} cn
===============================================================================================
About -- Biography -- Events -- Publications -- Teaching
===============================================================================================
Research Philosophy
My
research philosophy has consistently been driven by the dual aspiration of
devising effective models and algorithms to address real-world challenges while
distilling novel mathematical problems during this process. In essence, I aim
to contribute to both practical applications and the advancement of mathematics
itself. This dualism has served as the cornerstone of my research endeavors.
Areas of Focus
My
research has primarily focused on biomedical imaging, with a particular
emphasis on image reconstruction, image analysis, and using images and medical
data to aid in clinical decision-making.
More recently, I have also begun working extensively in machine learning
and artificial intelligence, particularly in the development of foundation
models for biomedical data analysis, automated reasoning, and scientific
computing. In particular, I have recently directed my
primary efforts toward fully advancing AI for Mathematics (AI4M), an emerging
and exciting research direction.
Earlier Career
During
my doctoral and postdoctoral years, I have developed various models and
algorithms within the frameworks of Partial Differential Equations (PDEs) and
wavelets. These include designing PDE models for cerebral aneurysm segmentation
to facilitate subsequent geometric measurement (Ref);
integrating the notion of PDEs, level-set methods and wavelet transforms to
create computational tools for cardiovascular plaque quantification (Ref);
formulating CT image reconstruction models by exploiting the property of sparse
approximation of wavelet frame transforms (Ref1,
Ref2,
Ref3);
and optimizing radiation therapy for cancer mathematically (Ref)
which was later reported by phys.org.
Unveiling the
Connection: PDEs and Wavelets
Throughout
the course of addressing these applied problems, I became increasingly aware of
the striking algorithmic resemblance between PDEs and wavelets. This led to an
investigative journey with collaborators to explore any intrinsic relationships
between these two paradigms, which had evolved independently in the field of
imaging for nearly three decades. We discovered profound connections,
unsettling traditional views and establishing an asymptotic convergence
relationship between wavelet-based optimization models and PDE models. (Ref1,
Ref2,
Ref3,
Ref4)
This theoretical insight effectively bridged the geometric interpretations of
differential operators with the sparse approximations and multi-scale nature of
wavelets, inspiring new models that amalgamated the strengths of both PDEs and
wavelets. In particular, this insight has led to new wavelet frame-based image
segmentation models for medical images (Ref).
Notably, our collaborative paper on wavelet frame-based segmentation of
ultrasound videos (Ref)
with my colleagues at Shanghai Jiao Tong University and National University of
Singapore gained media attention, including coverage by SIAM
News, Science
Daily, etc.
Journey into Machine
Learning
My
initial venture into machine learning commenced in 2014 resulting in a
sole-authored paper that introduced wavelet frames into semi-supervised
learning models on graphs and point clouds (Ref),
as well as a work on sparse linear discriminant analysis with my colleagues
from the statistics program at the University of Arizona (Ref).
However, it was not until 2015-2016 that I fully grasped the revolutionary
impact of deep learning, particularly on biomedical imaging problems. It was
also during this period that our earlier works on unveiling the connections
between PDEs and wavelets contributed to a unified perspective on these
mathematical models, which later informed our mathematical understanding of
deep neural networks.
Subsequently,
I led my team to pivot our focus towards deep learning methodologies. The core
motive has been to explore the algorithmic relations between traditional
mathematical methods like PDEs and wavelets and the data-driven models in deep
learning. This exploration culminated in two important works of mine between
2017 and 2018: the establishment of the link between numerical differential
equations and deep neural network architectures, leading to the development of
ODE-Net (Ref)
and PDE-Net (Ref1,
Ref2),
which were empirically validated on large-scale datasets. Through this and
several subsequent research studies, we gradually developed a novel generic
methodology for synergistically integrating mathematical modeling and machine
learning techniques. We have been constantly practicing and
refining this generic methodology in my research endeavors ever since (e.g.
examples in “Detour to Scientific Computing”).
The
core focus of my presentation at the 2022 International Congress of
Mathematicians (ICM) was to elucidate the intricate connections between PDEs
and wavelets, as well as the links between discrete differential equations and
deep neural networks. These “bridges” have intriguing
implications for the fields of computational imaging and scientific computing,
which were thoroughly discussed in my talk and the
corresponding proceedings and notes (Ref1, Ref2).
−
Machine
Learning for Scientific Computing：Upon
understanding deep neural networks through the lens of numerical differential
equations, it became natural to tackle challenges in scientific computing,
specifically, PDE-based forward and inverse problems. For the forward problems,
we blended numerical methods for conservation laws and multigrid methods with
deep reinforcement learning and meta-learning. (Ref1, Ref2) More recently, we discovered
a connection between meta-learning and reduced-order modeling, paving the way
for a new technique in approximating the solution manifold of parametric PDEs.
(Ref1, Ref2) For inverse problems, our
focus has been primarily on imaging, where we proposed several ways of melding
deep learning techniques with traditional mathematical algorithms (Ref1,
Ref2, Ref3, Ref4).
−
Clinical
Applications and Translational Research：Since 2019, I have embarked on an extensive collaboration with Peking
University Cancer Hospital, focusing on clinical auxiliary diagnostic issues.
This has resulted in a series of exciting progresses in medical image analysis,
contributing valuable tools for clinical practice that have seen successful
adoption and some degree of translational implementation.(Ref1, Ref2, Ref3,
Ref4, Ref5)
AI for Mathematics:
Toward Rigorous, Verifiable Intelligence
AI for Mathematics
(AI4Math) is, in my view, best understood against the long-term evolution of
mathematical research itself. Historically, mathematics has been driven by two
intertwined pillars: axiom-based deductive reasoning, which underlies much of foundational
mathematics, and scientific computing, where numerical methods enable the
quantitative exploration of complex systems across the natural and engineering
sciences. The rapid development of modern AI is now reshaping both pillars in a
profound way, marking a broader transition from problem-specific modeling
toward increasingly general-purpose modeling. In scientific computing,
data-driven approaches—ranging
from high-dimensional function approximation and operator learning to
architectures that fuse physical structure with data—are
changing how we approach high-dimensional PDEs, multiscale modeling, and
challenging inverse problems (including computational imaging and biomedical
data analysis). In deductive reasoning, long-standing barriers caused by
combinatorial explosion in symbolic logic and search are being revisited
through the emerging synergy between large language models and formal systems,
opening new possibilities in automated theorem proving, auto-formalization, and
computer-assisted exploration of abstract mathematical structures. Together,
these developments suggest that computational tools are no longer confined to
numerical simulation; they are beginning to participate—at least in constrained, verifiable ways—in
logical derivation and structural discovery, offering new pathways toward
mathematical problems of higher dimensionality and complexity.
In the past few years, as I
began engaging more deeply with this emerging landscape, I also became
increasingly aware of a fundamental gap between the impressive breadth of today’s general-purpose AI systems and
the specific demands of mathematical research. While foundation models can
perform remarkably well on a wide range of multimodal and language tasks, using
them directly in mathematics exposes clear bottlenecks at a more structural
level: on the reasoning side, the lack of strict logical constraints makes
hallucinations and ungrounded leaps difficult to avoid; on the computation
side, the sensitivity required to perceive and respect conservation laws,
invariances, and high-precision numerical mechanisms remains limited. In this
sense, existing general models are not designed for mathematics as a native
habitat, and simply “applying”
them often fails to reach the core of what mathematicians and scientific
computing practitioners truly need. This realization led me to a more ambitious
commitment: rather than treating AI as an external tool to be adopted, I became
convinced that we must build a mathematics-native intelligence substrate—one that integrates rigorous logical verification and high-fidelity
numerical feedback into a unified environment. Such environments offer
unusually strong and unambiguous supervision signals—whether
through the deterministic state-checking and proof validation in formal systems
such as Lean, or through invariant
structures and energy-based constraints in physical and mathematical models—providing what I see as a principled pathway to restrain model
stochasticity and push beyond the capability boundary of general-purpose AI.
Building on this
perspective, I have come to view AI4M not as a one-way application of AI to
mathematics, but as an inherently bidirectional and self-reinforcing process—one that “strengthens
AI with mathematics, and in turn advances mathematics with AI.” On the one hand, mathematics offers AI a uniquely rigorous
cognitive scaffold: the way mathematicians learn, generalize, and verify can
inspire more structured training curricula, richer evaluation axes (beyond
surface accuracy), and principled approaches to interpretability that probe the
internal mechanisms of reasoning rather than merely its outputs. On the other
hand, as models become increasingly grounded in logical verification and
mechanistic constraints, they can begin to serve as more than productivity
tools—evolving toward research partners that help
explore unfamiliar proof pathways, translate informal ideas into formal
statements, and tackle high-dimensional scientific computing problems that
strain classical methods. In my mind, the long-term promise of AI4M lies
precisely in this closed loop: mathematical certainty and structure providing
the “hard feedback” that
reshapes AI systems, while increasingly capable AI systems return that value by
expanding the frontier of what is feasible in both deductive discovery and
computational mathematics.
(See our recent review, and
the very first in literature, on AI4Math. AI for Mathematics: Progress,
Challenges, and Prospects)
What we have built so
far reflects this unified vision:
−
Scientific
Computing: In the “computation” pillar of AI4M, my group has been building foundation models for
PDE solving that can efficiently support a wide range of downstream tasks. A
key milestone is that we first observed, in the 1D setting, a scaling law for
learning a general PDE solution operator—suggesting
that operator-level generalization may emerge predictably with increasing
data/model/compute (Ref1, Ref2). Building on this, we have
recently extended the model to 2D (Ref),
and are continuing to broaden the pretraining distribution while actively
seeking concrete real-world application scenarios where such a PDE foundation
model can deliver clear advantages over classical pipelines.
−
AI
inspiring pure mathematics research: On the “reasoning” pillar, our work has explored how
AI can meaningfully participate in highly abstract mathematical discovery—not by replacing proof, but by guiding human intuition toward
structures that are difficult to see unaided. One representative example arises
from arithmetic geometry and representation theory, where affine Deligne–Lusztig varieties (ADLV) play a central role in the geometric
realization of the Langlands program. The dimension computation of ADLV, as a
key invariant, depends on intricate combinatorial structures of affine Weyl
group elements and has long lacked a truly general explicit characterization.
By analyzing large-scale geometric/combinatorial data with machine learning
models, we not only “rediscovered” the classical dimension formula, but also detected systematic
patterns of deviation in boundary regimes where existing theory fails, and
further proved a new theorem giving a lower bound on the actual dimension,
filling a long-standing quantitative gap in the field. In my view, this
provides an early and concrete validation of the AI4M path of human–AI collaborative exploration in deep, abstract areas of algebra and
geometry. (Ref)
−
Formal
reasoning infrastructure:
To make AI-assisted deductive mathematics reliable rather than merely
fluent, we have built an end-to-end infrastructure around Lean that connects
retrieval, data/benchmarks, and neuro-symbolic proving—addressing hallucination under weak
constraints, scarcity of formal data, and the difficulty of proof search. Our
approach is intentionally end-to-end: we connect retrieval (to ground
generation), data/benchmarks (to train and measure), and neuro-symbolic proving
(to close the generate–verify loop) into a single,
continuously improving ecosystem.
Mathematical Information Retrieval (MIR): We have been building retrieval
infrastructure that spans both formal and informal sides of mathematical
knowledge. On the formal side, LeanSearch
targets cross-modal semantic alignment between natural language and formal code
(Ref), so that informal queries
(or partially formalized proof states) can retrieve relevant theorems, lemmas,
and proof patterns from large formal libraries; by being deeply integrated into
Lean's official mathlib4 ecosystem, LeanSearch serves not only as a user-facing
tool for mathematicians, but also as an enabling component for
retrieval-augmented autoformalization and prover agents. On the informal side,
we developed Matlas, a semantic
retrieval system indexing millions of mathematical statements harvested from
arXiv and other open resources, enabling large-scale cross-domain discovery of
non-trivial connections between seemingly distant subfields (Ref). Together, LeanSearch and
Matlas provide a principled way to “anchor” generation in existing verified
knowledge and to surface latent structural links across the mathematical
literature.
Datasets and Benchmarks: Recognizing that progress in
autoformalization and formal reasoning is constrained by both data quality and
evaluation realism, we released Herald, an auto-formalization dataset oriented
toward high-difficulty competition mathematics, together with a supporting
translation/evaluation toolchain (Ref).
Building on this, we developed Aria, an autoformalization agent that translates
even more challenging informal problems into formally checkable statements,
helping bridge the gap between model outputs and verifiable formal artifacts (Ref). In parallel, we introduced
FATE (M/H/X) as an algebra-focused evaluation suite designed to probe formal
reasoning beyond short, template-like proofs—emphasizing depth, structure, and robustness under
challenging settings (Ref). We
also contributed to competition-grade data efforts through the Numina team—including the collection and curation of high-quality Olympiad-style
problems for AIMO (Ref).
Collectively, these resources serve two roles: (i) as training and diagnostic
substrates for models intended to operate in both formal and informal
environments, and (ii) as community benchmarks that make comparison and
iteration scientifically meaningful.
Neuro-symbolic formal proving: We further developed REAL-Prover (Ref), combining the “intuition”
of large models with the rigor of symbolic solvers, and built the associated
tactic-generation tool reap (Ref),
which is being tested and maintained as an official candidate tactic within
mathlib4.
−
Math
research agents: from
informal exploration to verified proof. Building on the retrieval tools,
data, and neuro-symbolic proving infrastructure above, we have been developing
research-oriented agents that engage with open mathematical problems
end-to-end, coupling informal exploration with formal verification. Rethlas is an informal
mathematical research agent built on top of Matlas: given an open
conjecture, it leverages large-scale semantic retrieval to surface candidate
pathways and non-trivial connections across subfields, proposing informal proof
sketches that human experts typically reach only through extended
cross-disciplinary dialogue. Archon
is its formal counterpart — a Lean-based autoformalization and proving agent that turns
informal proof sketches into machine-checkable formal artifacts, with LeanSearch
integrated as a native tool in its decision loop.
As an independent demonstration
of Archon's formal capability, we applied it to the AI-generated proofs by
OpenAI on the FirstProof
benchmark of ten research-level problems. Archon autonomously produced
end-to-end Lean 4 formalizations (approximately 8,800 lines each, zero sorry)
for Problems 4 and 6 —
notably the two problems that DeepMind's Aletheia had not been able to settle,
suggesting a non-trivial level of formalization difficulty (technical report
& outputs
of Archon on P4 and P6).
As a further demonstration
of this pipeline, Rethlas identified a non-trivial connection between
quasi-completeness theory and Jensen's formal fiber construction, which Archon
subsequently realized as a roughly 19,000-line Lean 4 proof (zero sorry) resolving
D.D.
Anderson's 8a conjecture, an open problem that had been standing since
2014 (technical report & outputs of the agents).
This line of work
illustrates how retrieval, autoformalization, and neuro-symbolic proving can be
composed into a single system capable of contributing verifiable progress on
genuine research-level mathematics.
−
Mechanistic
interpretability:
Parallel to building AI4Math systems, I have also been pursuing a more
foundational motivation: to understand the inner workings of LLMs by examining
their activity when they carry out high-level cognitive tasks, especially
reasoning. Doing so requires interpretability tools that can decipher the
meaning encoded in high-dimensional objects—activations, attention pathways, and internal states—at a scale where systematic conclusions become possible. This
motivation has led to two recent works. Hierarchical Sparse Autoencoders (HSAE)
provide a scalable way to uncover multi-level conceptual hierarchies inside
model representations, revealing how high-level notions may decompose into more
fine-grained features across layers (Ref).
InverseScope offers an assumption-light route to interpret activations by
characterizing the space of inputs consistent with a target internal state,
enabling quantitative testing of hypotheses about what information that state
encodes (Ref). Together, these
tools move interpretability beyond isolated features toward a more structured
and testable understanding of reasoning-related representations, and we will
continue improving them to support increasingly mathematical and symbolic
accounts of how LLMs implement complex cognition.
Last updated: 04/2026.