I'm interested in a computer program, possibly a web app, that could prove theorems and show its proofs.
I essentially want to type in a theorem like "For every bounded sequence, there exists a subsequence that has a limit" and see a proof for that.
I googled theorem provers, and I found Lean with this tutorial, I found HOL and E, but looking at their websites, it seems very complicated. The tutorial I linked to shows the Lean language, which is a whole thing. I was expecting either human language or mathematical language. (Like ∃ and ∀.)
Does something like that exists?
There's no perfect solution. Finding a proof of an arbitrary statement is undecidable, finding a proof of bounded length is NP-complete. Perhaps one day we'll have a program that heuristically is as good as a human mathematician, but we're nowhere close.
There's a system called Mizar. Here's how you write irrationality of e http://www.mizar.org/JFM/Vol11/irrat_1.abs.html, and as far as I see this is rendered nicely as a PDF http://www.mizar.org/JFM/pdf/irrat_1.pdf.
Proof assistants such as Coq, Agda. Perhaps you might not see ∃ and ∀ in descriptions of those systems, but let this not deter you: they are based on calculus of constructions or type theory, not on first-order logic. Coq was used to formalize the four color theorem, the odd order theorem, and a formally correct C compiler. Proving a statement becomes an interaction: the proof assistant shows the assumptions and you guide it towards the goal; if it's simple enough, you can use a tactic "this is trivial" and the computer will fill the rest.
Regarding human language, there was a program that solved a limited range of problems in metric spaces and returned a text output that was not easily distinguishable from a human proof https://arxiv.org/pdf/1309.4501.pdf.