Shuoming Deng

From Lecture Notes to Lean: Formalizing a Textbook on Probability Theory

As large language models become increasingly capable of generating mathematical arguments, mathematics is likely to face not a scarcity of proofs but an abundance of plausible ones. In such an environment, verification, exposition, and incorporation into reusable mathematical infrastructure become central tasks. We rep...