Project VD: Formalizing Value Distribution Theory of Complex Analysis

Abstract: We present "Project VD", an effort to formalize value distribution theory in the Lean theorem prover. Pioneered by Nevanlinna (and others) in the 1920s, the theory studies how complex-analytic and meromorphic functions distribute their values, providing a quantitative measure of their complexity. Beyond its intrinsic interest, the theory gained wider significance after Vojta found surprising connections between complex analysis and Diophantine geometry.

This talk will briefly introduce the main objects and report on the formalization work completed so far. Finally, I would like to pose several open design questions that have emerged during this project, hoping to start a discussion in the community.

logic in computer sciencemathematical softwareMathematics

Audience: researchers in the discipline

( slides | video )

Lean Together 2026