This is the repository for slides and short notes used for my talks. You are free to reuse the content under the terms of CC BY-SA 4.0.
proof-assistant: Proof assistants.lean-prover: The Lean functional programming language and proof assistant.lean-applications: Applications of Lean.mathlib4-porting: Porting Mathlib from Lean 3 to Lean 4.
learn-formal-math: Learning formalized mathematics.
cultural-policy: South Korea's regulations on producing, distributing, and viewing creative work and pornography.cysem-constitutional-complaint: Constitutional Complaint Against the Act on the Protection of Children and Youth Against Sex Offenses.proposed-amendment-to-act: My draft of an amendment to the Act on the Protection of Children and Youth Against Sex Offenses.