Autoformalization at scale

Stream: new members

[Michal Buran]

I’m curious about the current state of autoformalization as a way to build or extend Lean libraries. Is it good enough in principle, and if so, why isn’t it used more routinely? Are the main blockers pedagogical or cultural, cost, review and trust issues, tech-debt and maintainability, or the fact that library design involves many non-canonical choices? If it’s not good enough yet, what are the key obstacles? And if people are doing this already, what projects exist and how good are they?

[Michael Rothgang]

See #general > sloplib - this is being discussed. In short, autoformalisation is decent at proving theorems (but these proofs are still much longer than mathlib-level proofs, often not in the right generality, etc.), but it's very unclear if it can be useful for formalising definitions. The bottleneck with formalising a lot of mathematics are definitions, and these need human review and experimentation.