AI, Data Science & Cloud Certificates from Google, IBM & Meta — 40% Off
One plan covers every Professional Certificate on Coursera. 40% off Coursera Plus Annual.
Unlock All Certificates
Explore elementary number theory concepts through formal mathematical proof using the Lean theorem prover in this conference talk. Learn how to formalize undergraduate-level number theory problems including rings, unique factorization domains, congruence relationships, finite fields, and quadratic reciprocity within the Lean programming environment. Discover practical approaches to translating traditional mathematical reasoning into formal proofs while working with the Mathlib library. Gain insights into the intersection of computational proof verification and classical number theory through hands-on examples and demonstrations that bridge theoretical mathematics with modern formalization techniques.
