This talk shares the challenges I faced when formalizing set theory axioms from lecture notes in Lean. In such a rigorous proof assistant, every step must be explicit: for example, if you prove ∃ x, P(x) is true, how do you actually use the x? How should notations be defined, and which lemmas must come first to state other definitions correctly? Concepts that seem “clear” on paper can become unclear in Lean, highlighting the interest and value of formalization. I hope the audience gains insight into the motivation behind Mathlib definitions and learns how to address these issues when writing their own definitions in Lean.

• 書面報告

• 3分鐘簡介影片

• 研討會15分鐘報告影片