Marijn Heule | |
---|---|

Born | |

Alma mater | Delft University of Technology |

Occupation | Associate professor |

Employer | Carnegie Mellon University |

Known for | Using SAT solvers to solve mathematical conjectures |

Website | http://www.cs.cmu.edu/~mheule/ |

**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. Heule has used these solvers to resolve mathematical conjectures such as the
Boolean Pythagorean triples problem,
Schur's theorem number 5, and
Keller's conjecture in dimension seven.

Heule received a PhD at
Delft University of Technology, in the
Netherlands, in 2008. He was a research scientist, later a research assistant professor, at the
University of Texas at Austin from 2012 to 2019. Since 2019, he has been an associate professor in the Computer Science Department at
Carnegie Mellon University.^{
[2]}

In May 2016 he, along with Oliver Kullmann and Victor W. Marek, used SAT solving to solve the
Boolean Pythagorean triples problem.^{
[3]}^{
[4]} The statement of the theorem they proved is

**Theorem** — The set {1, . . . , 7824} can be partitioned into two parts, such that no part contains a Pythagorean triple, while this is impossible for {1, . . . , 7825}.^{
[5]}

To prove this theorem, the possible colorings of {1, ..., 7825} were divided into a trillion subcases using a
heuristic. Each subclass was then solved a
Boolean satisfiability solver. 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).^{
[5]} The paper describing the proof was published in the SAT 2016 conference,^{
[5]} where it won the best paper award.^{
[5]} A $100 award that
Ronald Graham originally offered for solving this problem in the 1980s was awarded to Heule.^{
[3]}

He used SAT solving to prove that
Schur number 5 was 160 in 2017.^{
[4]}^{
[6]} He proved
Keller's conjecture in dimension seven in 2020.^{
[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]}

**^**Calmthout, Martijn van (June 6, 2016). "Bewijs dat nét op 200 laptops past" (PDF).*de Volkskrant*(in Dutch). p. 23. Archived (PDF) from the original on January 5, 2022. Retrieved May 11, 2021.- ^
^{a}^{b}Heule, Marijn (August 20, 2019). "Marijn J.H. Heule" (PDF).*www.cs.cmu.edu*. Retrieved June 15, 2021.`{{ cite web}}`

: CS1 maint: url-status ( link) - ^
^{a}^{b}Lamb, Evelyn (May 26, 2016). "Two-hundred-terabyte maths proof is largest ever".*Nature*.**534**(7605): 17–18. Bibcode: 2016Natur.534...17L. doi: 10.1038/nature.2016.19990. PMID 27251254. - ^
^{a}^{b}Hartnett, Kevin. "Computer Scientists Attempt to Corner the Collatz Conjecture".*Quanta Magazine*. Retrieved March 8, 2021.`{{ cite web}}`

: CS1 maint: url-status ( link) - ^
^{a}^{b}^{c}^{d}Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W. (2016). "Solving and Verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer". In Creignou, Nadia; Le Berre, Daniel (eds.).*Theory and Applications of Satisfiability Testing – SAT 2016: 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings*. Lecture Notes in Computer Science. Vol. 9710. pp. 228–245. arXiv: 1605.00723. doi: 10.1007/978-3-319-40970-2_15. **^**Heule, Marijn J. H. (2017). "Schur Number Five". arXiv: 1711.08076 [ cs.LO].- ^
^{a}^{b}Hartnett, Kevin. "Computer Search Settles 90-Year-Old Math Problem".*Quanta Magazine*. Retrieved March 8, 2021.`{{ cite web}}`

: CS1 maint: url-status ( link) **^**Subercaseaux, Bernardo; Heule, Marijn J. H. (January 23, 2023). "The Packing Chromatic Number of the Infinite Square Grid is 15". arXiv: 2301.09757 [ cs.DM].**^**Hartnett, Kevin (April 20, 2023). "The Number 15 Describes the Secret Limit of an Infinite Grid".*Quanta Magazine*. Retrieved April 20, 2023.