So I got an email from one of my colleagues on the Collatz Conjecture with a link to the article *[Computer Scientists Attempt to Corner the Collatz Conjecture](https://www.quantamagazine.org/can-computers-solve-the-collatz-conjecture-20200826/)* by Kevin Hartnett in Quanta Magazine.


On digging through the conjecture, it seems it is not even known it is a $\Pi\_1$ or $\Sigma\_1$ statement. See the Math.StackExchange question [Is the Collatz conjecture in $Σ\_1/Π\_1$?](https://math.stackexchange.com/questions/100218/is-the-collatz-conjecture-in-sigma-1-pi-1). For more information we can find details in the following thesis:


* Matthew Alexander Denend, *Challenging variants of the Collatz Conjecture*, Masters Thesis, The University of Texas at Austin 2018, doi:[10.26153/tsw/1559](https://doi.org/10.26153/tsw/1559).


Does it mean they have already shown Collatz is a $\Sigma\_1$ statement?



Does this prove Collatz is a $\Sigma_1$ problem?
It seems I was wrong - see Emre Yolcu's comment below.
------------------------------------------------------




---


My understanding is that that has **not** been accomplished (although the Quanta article is pretty vague so I could be misunderstanding the situation).


The Quanta article describes the following process:


* Whip up a rewriting system which always terminates iff Collatz is true. This has been successfully done - but note that the termination problem is a priori $\Pi^0\_2$, just like Collatz.
* Try to find a collection of matrices satisfying some complicated constraints relating to that rewriting system. **This** is the task which SAT solvers are relevant for. However, they have not yet found an appropriate collection of matrices.
* ***(This is where I was wrong:)*** ~~Even after finding such a collection, we're not done. All that this will accomplish is reduce Collatz to a particular problem about matrix multiplication *(which the Quanta article doesn't state - moreover, it doesn't explain why that problem should be more tractable than the rewriting one or the original Collatz conjecture)*.~~


Re: that third bulletpoint, I think that there's a particular part of the article which is potentially confusing:



> 
> “You try to find matrices that satisfy these constraints,” said Emre Yolcu, a graduate student at Carnegie Mellon who is working with Heule on the problem. “If you can find them, you prove [they’re] terminating,” and by implication, you prove Collatz.
> 
> 
> 


~~It would have been clearer to write "If you can find them, you **then try to prove** [they're] terminating, **and if you can** you prove Collatz." That is, finding a system of matrices satisfying the given constraints - which is indeed $\Sigma^0\_1$ - is only the first step, and the remaining fact we need to prove is presumably still $\Pi^0\_2$.~~


Actually it seems I got that exactly wrong!


That said, pending further elaboration from Emre we may only have a $\Sigma\_1$ sentence which *implies* Collatz - I don't know if the nonexistence of an appropriate matrix family would imply that Collatz fails.


