Post #1782143
2026-04-28 06:14 UTC
@vnikolov
They show,
(implies (rationalp x)
(not (equal (* x x) 2)))
@simon_brooke
Replies (1)
-
@vnikolov@ieji.de 2026-04-28 06:37
@screwlisp wrote: «They show, (implies (rationalp x) (not (equal (* x x) 2)))» Thank you. I read this as ACL2's representation of the (trivial) theorem that no rational number is a root of x² = 2. @simon_brooke