What don't they instead work from the opposite direction:
Create an abstract model of a Collatz loop that doesn't end with 1(instead looping back to same number) and prove it can't exist(Reductio ad absurdum).
This approach has been explored. It has only been helpful for showing that certain types of (short-ish) cycles can't occur [1]. Showing that the sequence can't get larger and larger forever (without repeating) with this approach has been a non-starter.
