When I was in high school in 2012, I read the formal definition of a function on Wikipedia and it blew my mind. One year later, I dropped out of high school and tried to rigorously define everything in high school mathematics from scratch.

Of course, it didn't work, although I gained some basic knowledge about propositional logic and predicate logic. In 2014, I discovered Metamath's set.mm database, but I didn't have the time to thoroughly understand it. Since 2022, I've been learning and using the Lean theorem prover and Mathlib.

When I try to write a proof on paper, it takes as much time as writing a formal proof. That's because I end up writing a semi-formal proof without using a proof assistant. I'm not sure why, but I feel like I'm in full control of mathematical concepts when I use proof assistants.