To quickly summarize: A Turing machine program or method can't solve the Entscheidungsproblem, which means you can't have a general algorithm to prove all possi

To quickly summarize: A Turing machine program or method can't solve the Entscheidungsproblem, which means you can't have a general algorithm to prove all possible statements true or or false (or equivalent) within a formal system. For example you can't have a general program that you feed in any 2 mathematical statements and tells you if they're equal. From what I understand this is proven for "regular math" but not all formal systems. As a counterpoint, there are many algorithms these days that can do theorem proving better than anything before in history (partly thanks to AI, and partly thanks to the massive efforts that went into symbolic computation engines over the past decades). I think in a few years theorem proving will be done elegantly by computers instead of humans. Not all theorems, sure, but this is the world we got to live in.