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

Shuo Deng, Kenneth W. Shum

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…