I Lean-ed into Formalization first time

I was fascinated when one of my Professors, Siddhartha Gadgil at Indian Institute of Science gave a talk where he should machines checking proofs. This is not AI. Rather a programming language. I was in my first year in undergrad when I saw this and ...