In my Real Analysis class in college I remember seeing the proof that rational numbers are countable via a diagonalisation argument. Proving something is true and implementing a counting algorithm that will assign any given Rational a unique positive integer are two very different things. This link is class room explanation behind all the math without dumbing anything down. Here’s the original amazing paper by virtue of simplicity and elegance. The only things needed to understand it is the most rudimentary understanding of binary trees and Euclid’s gcd algorithm. I wrote up some scheme code to print out the “parents” of the node, which allows one to assign a unique positive integer to every/any Rational.
;Tree
(define (display-all args)
(if (null? args)
(display "\n")
(begin (display (car args))
(display " ")
(display-all (cdr args)))))
(define (p-parents m n)
(cond ((or (zero? m) (zero? n)) #t)
((= m n) (begin (display-all (list 1 "\n")) ""))
((< m n) (begin (display-all (list m " " n "\n")) (p-parents m (- n m))))
((> m n) (begin (display-all (list m " " n "\n")) (p-parents (- m n) n)))))
;Print the parent nodes of 49/19
(p-parents 49 19)