Formalization

I have recently become interested in formalizing mathematics in Lean. I am currently contributing to the Hodge Conjecture formalization project, which was initiated at the Formal Conjectures workshop.

In near future, I plan to formalize the abundance conjecture, as well as the proof of the abundance conjecture in dimension three over the complex numbers.