If you are interested in the course, please fill out this form; it should take 2 minutes, does not commit you to anything if you later change your mind, and is only meant to help with organization.

This specialized course introduces Lean and familiarizes students with the formalization of mathematics in a proof assistant. Participants gain hands-on experience coding mathematical objects, stating theorems, and formally verifying proofs. The course covers Lean and its mathematical library (mathlib), type theory, and the interplay between AI and mathematics. Advanced mathematical topics may include number theory, general topology, commutative algebra, or algebraic geometry, depending on the interests of the group. No specific prerequisites are required, and no prior knowledge of programming or logic is needed.

More material will be available here soon.