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).