Can Computers Prove Theorems?

Only if contexts are defined and logically comparable. Otherwise it will just risk or tilt on question like any other human, until the risk taken take down the problem to increase the definitions. The right question would be: can computers define concepts(names for numbers) by itself? Would you trust while it makes you happy or will you investigate by yourself the magic?

Also related: https://news.ycombinator.com/item?id=21362470

Lean has been going hard at PR at the moment.

I would really like to dip my toe into the theorem proving waters from a scientific/mathematical perspective.

I'm not sure whether to start with Coq, Agda, Isabelle or Lean. Does anyone on HN have a feeling as to a sensible one to start with?

Start with the one with the best documentation. It's hard to beat Software Foundations: https://softwarefoundations.cis.upenn.edu/, which happens to be for Coq.

If you search the web for "Software Foundations in X", you will find partial ports of some of the initial chapters to pretty much any other proof assistant. Maybe nowadays they are full, complete ones that would allow you to use Isabelle or Lean instead.

Lovely poem.

One reading of it is something like "if computers can't prove that computer proofs are always correct, then we can't be sure of anything", but that is true of human proofs as well, so we might as well Ctrl-W mathematics itself.

Another reading is something like "this very introductory article didn't mention whether we can formalize Gödel's incompleteness results in the computer, so it's too introductory for me". Fair enough.