[umutisik]

Real life use cases for theorem proving I am aware of: - Formal verification of implementations for applications that require extreme security and reliability. (banking, aerospace, ...) - Automated theorem proving would increase the pace of theoretical work. In some cases, that helps guide useful work. There are better examples, but a simple one: nobody is looking for faster (worst-case) sorting algorithms because there is a proven theoretical limit. Don't believe in theory, but don't be without theory! It definitely won't hurt if theory-building is cheaper and faster.

Also, it's the most complicated pure reasoning task you can build. So working on theorem-proving AI may help in reasoning and reliability.