Starting from literally nothing, it derived all of the geometric propositions in Euclid's Elements in a matter of seconds.
Where do you get these detailed claims about the program?
Just to point out the obvious, your first link certainly does say that
Once you know the ansatz, you can have the machine, discover from scratch all the statements of any bounded complexity, and prove them at the same time, either rigorously (time permitting) or semi-rigorously (if a polynomial of degree 10^100 vanishes at 10^6 random values it is most likely identically zero, just like Rabin's pseudo-primes). This is what Shalosh B. Ekhad, XIV, did in its 2050 PLANE GEOMETRY TEXTBOOK. What is so nice about it is that it is written in a precise, and hence completely formally correct programming language, Maple, but the names of the definitions are English based. Also each statement doubles as the proof, ready to be executed by Maple. So we have a text that is even more formally correct than any logocentric human proof (recall that Bill Thurston said that a computer program is much more formally correct than a human proof), yet just as much fun to read, and in which once you read the statement, you already have the proof (modulo running it on Maple, but I already did, so you can trust me and not run it again).
Oh, yeah, I missed that Zeilberger used the phrase "from scratch," so that explains why JH says "from literally nothing" (though I disagree), but why did you quote the rest of the passage? Do you think it suggests any other of JH's claims?
In a recent comment thread I expressed skepticism as to whether there's been meaningful progress on general artificial intelligence.
I hedged because of my lack of subject matter knowledge, but thinking it over, I realized that I do have relevant subject matter knowledge, coming from my background in pure math.
In a blog post from April 2013, Fields Medalist Timothy Gowers wrote:
I don't know of any computer programs that have been able to prove theorems outside of the class "very routine and not requiring any ideas," without human assistance (and without being heavily specialized to an individual theorem). I think that if such projects existed, Gowers would be aware of them and would likely have commented on them within his post.
It's easy to give an algorithm that generates a proof of a mathematical theorem that's provable: choose a formal language with definitions and axioms, and for successive values of n, enumerate all sequences of mathematical deductions of length n, halting if the final line of a sequence is the statement of the the desired theorem. But the running time of this algorithm is exponential in the length of the proof, and the algorithm is infeasible to implement except for theorems with very short proofs.
It appears that the situation is not "there are computer programs that are able to prove mathematical theorems, just not as yet as efficiently as humans," but rather "computer programs are unable to prove any nontrivial theorems."
I'll highlight the Sylow theorems from group theory as examples of nontrivial theorems. Their statements are simple, and their proofs are not very long, but they're ingenious, and involve substantive ideas. If somebody was able to write a program that's able to find proofs of the Sylow theorems, I would consider that to be strong evidence that there's been meaningful progress on general artificial intelligence. In absence of such examples, I have a strong prior against there having been meaningful progress on general artificial intelligence.
I will update my views if I learn of the existence of such programs, or of programs that are capable of comparably impressive original research in domains outside of math.