An alternative proof that the Fibonacci group F(2,9) is infinite
Derek F. Holt · arXiv (Cornell University) · 1995
This note contains a report of a proof by computer that the Fibonacci group F(2,9) is automatic. The automatic structure can be used to solve the word problem in the group. Furthermore, it can be seen directly from the word-acceptor that the group generators have infinite order, which of course implies that the group itself is infinite.