Yes, it's a theorem proving system, and it's based on foundations that are powerful enough to represent all of (formal) math. Including something like Lean exc

Yes, it's a theorem proving system, and it's based on foundations that are powerful enough to represent all of (formal) math. Including something like Lean excludes math itself from being able to do "specific concrete computations," which is absurd. Here are some examples to give you an idea of concrete calculations. Lean is not a CAS, so it needs some help in the form of tactic proofs (which are unreadable without an IDE, but their structure sort of mirrors work you'd do on paper): import data.real.basic import data.real.sqrt import tactic -- that 2^2 - 2 = 0 example : (real.sqrt 2)^2 - 2 = 0 := by norm_num -- that if x solves x^2 - 2x + 1, then x = 1. example (x : ℝ) (h : x^2 - 2*x + 1 = 0) : x = 1 := begin have : x^2 - 2*x + 1 = (x - 1)*(x - 1), ring, rw this at h, cases eq_zero_or_eq_zero_of_mul_eq_zero h with h' h', repeat { convert_to x - 1 + 1 = 1, norm_num, rw h', norm_num, }, end These were just some quick examples, but what I'm trying to show you is that in Lean you are working with the real numbers. They're just as real as the ones defined in a real analysis textbook, maybe moreso. They're just more tedious to deal with because the computer needs every calculation to come with some sort of proof of correctness, which thankfully can be filled in automatically sometimes with tactics like norm_num. (A meta-comment: I'm not sure why if you're not familiar with Lean you'd tell me what it can and cannot do. Maybe someone told you at some point "theorem prover systems prove general theorems" or "theorem provers can only prove things about computable reals" and you had no reason to believe that they weren't telling you the whole story? Don't take this too seriously, I'm just riffing on your original point.) p.s. Looking back to the beginning of this thread, I realize my saying "I'm not understanding what all the fuss is" could be misinterpreted -- I didn't meant to refer to you in particular. This was meant to be in the context of all the comments and the original article, and somehow I ended up replying to yours. Maybe one thing that caught my eye was the idea that there was much to unlearn here, but I ended up not addressing that point because I didn't have anything cogent to say. I think the sibling comment put it well, that there's value in learning to unlearn.