(auto)formalization, but why

Seewoo Lee, postdoc at EPFL. I want to share some thoughts on (auto)formalization based on personal experience, and propose some possible positive and negative usages of it. Disclaimer: I mostly focus on formalizations in Lean, due to my limited experience and knowledge. But most of the discussion can be applied to formalizations using other proof […]