Marienus Johannes Hendrikus Heule (born March 12, 1979, at Rijnsburg, The Netherlands)[1][2] is a Dutch computer scientist at Carnegie Mellon University who studies SAT solvers.
Since 2019, he has been an associate professor in the Computer Science Department at Carnegie Mellon University.
Creating the proof took about 4 CPU-years of computation over a period of two days on the Stampede supercomputer at the Texas Advanced Computing Center and generated a 200 terabyte propositional proof (which was compressed to 68 gigabytes in the form of the list of subcases used).
[7] In 2018, Heule and Scott Aaronson received funding from the National Science Foundation to apply SAT solving to the Collatz conjecture.
[7] In 2023 together with Subercaseaux, he proved that the packing chromatic number of the infinite square grid is 15[8][9]