Marijn Heule

From Wikipedia, the free encyclopedia

Marijn J. H. Heule
Born12 March 1979
Rijnsburg, The Netherlands
OccupationAssociate professor
EmployerCarnegie Mellon University
Known forUsing SAT solvers to solve mathematical conjectures

Marijn J. H. Heule (full name Marienus Johannes Hendrikus Heule, born 12 March 1979 at Rijnsburg, The Netherlands)[1][2] is a Dutch computer scientist at Carnegie Mellon University. Heule has developed SAT solving proofs to solve mathematical problems, including the Boolean Pythagorean triples problem, Schur's theorem number 5 and Keller's conjecture in dimension seven.

Career[]

Visualization of a solution of the Pythagorean Triples Problem

Heule received a PhD at Delft University of Technology, in the Netherlands, in 2008, and has been both research assistant professor at the University of Texas at Austin and an associate professor in the Computer Science Department at Carnegie Mellon University.[3][4]

In May 2016 he solved Boolean Pythagorean triples problem through a computer-assisted proof, SAT solving, along with Oliver Kullmann and Victor W. Marek.[5][6] The statement of the theorem 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}.[7]

There are 27825 ≈ 3.63×102355 possible coloring combinations for the numbers up to 7825. These possible colorings were logically and algorithmically narrowed down to around a trillion (still highly complex) cases, and those were examined using 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.[clarification needed]

The paper describing the proof was published in the SAT 2016 conference,[7] where it won the best paper award.[7] In the 1980s Ronald Graham offered a $100 prize for the solution of the problem, which was awarded to Heule.[5]

He also used the SAT solving computerized proof technique for solving Schur number 5 in 2017 and Keller's conjecture in dimension seven in 2020.[6][8]

In 2018, Heule and Scott Aaronson received funding from the National Science Foundation to apply SAT solving to the Collatz conjecture.[8]

Personal life[]

Heule is a native speaker of Dutch, a fluent speaker of English, a moderate speaker of German and French, and a basic reader of Latin, Classical Greek, and Classical Hebrew.[2]

References[]

  1. ^ "Marijn J.H. Heule" (PDF). Year of birth. Retrieved May 11, 2021.
  2. ^ Jump up to: a b Heule, Marijn (August 20, 2019). "Marijn J.H. Heule" (PDF). www.cs.cmu.edu. Retrieved June 15, 2021.
  3. ^ "Marijn J.H. Heule". cs.utexas.edu. Retrieved March 8, 2021.
  4. ^ "Marijn J.H. Heule". cs.cmu.edu. Retrieved March 8, 2021.
  5. ^ Jump up to: 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.
  6. ^ Jump up to: a b Hartnett, Kevin. "Computer Scientists Attempt to Corner the Collatz Conjecture". Quanta Magazine. Retrieved March 8, 2021.
  7. ^ Jump up to: a b c 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. 9710. pp. 228–245. arXiv:1605.00723. doi:10.1007/978-3-319-40970-2_15.
  8. ^ Jump up to: a b Hartnett, Kevin. "Computer Search Settles 90-Year-Old Math Problem". Quanta Magazine. Retrieved March 8, 2021.
Retrieved from ""