Learning theory studies when and how a learner can recover a useful rule from labeled examples. It sits at the intersection of combinatorics, measure theory, and both computational and statistical complexity theory.
Fix a domain \(X\), a set of labels \(Y\), and a hypothesis class \(\mathcal H \subseteq Y^X\). A learner takes a finite labeled sample and returns a candidate function:
The central questions are then mathematical ones: which hypothesis classes can be learned, what information a sample must contain, how complexity grows, and which measurability assumptions are needed to decide that a learner has succeeded.
One direction of the subject leads to machine learning, where the goal is to build practical algorithms that identify increasingly complex processes from increasingly unstructured data. The foundational direction asks what learning itself permits. Can learnability be decided in ZFC? How should complexity be defined over infinite sets? What happens to learning problems over non-Borel spaces? What logical and epistemological assumptions underlie a claimed endpoint of learning?
These questions reach well beyond machine learning. The same structures connect to model theory, computational geometry, measure theory, graph theory, and Banach space geometry, which makes formal learning theory a natural target for Mathlib.
In this talk, Dhruv will derive and formalize Pajor's inequality over infinite sets, explain its origins and role in Banach space geometry, and use it as a case study in what formalization reveals beyond a paper proof. He will close with open directions for research in formal learning theory and its development in Lean 4.
If time permits, the discussion will turn to a more speculative question: whether a neural network can be understood as a topological system that enriches sample-set complexity layer by layer, until it matches the complexity of the hypothesis class, and how a Lean formalization of a transformer might make that question precise.