Biography:Marijn Heule
Marijn J. H. Heule | |
|---|---|
| Born | 12 March 1979 Rijnsburg, The Netherlands |
| Occupation | Associate professor |
| Employer | Carnegie Mellon University |
| Known for | Using 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
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{{math 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]
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
- ↑ "Marijn J.H. Heule". Year of birth. https://www.cs.utexas.edu/users/marijn/VKN-583245.pdf.
- ↑ 2.0 2.1 Heule, Marijn (20 August 2019). "Marijn J.H. Heule". http://www.cs.cmu.edu/~mheule/resume.pdf.
- ↑ "Marijn J.H. Heule". https://www.cs.utexas.edu/users/marijn/.
- ↑ "Marijn J.H. Heule". http://www.cs.cmu.edu/~mheule/.
- ↑ 5.0 5.1 Lamb, Evelyn (May 26, 2016). "Two-hundred-terabyte maths proof is largest ever". Nature 534 (7605): 17–18. doi:10.1038/nature.2016.19990. PMID 27251254. Bibcode: 2016Natur.534...17L. http://www.nature.com/news/two-hundred-terabyte-maths-proof-is-largest-ever-1.19990.
- ↑ 6.0 6.1 Hartnett, Kevin. "Computer Scientists Attempt to Corner the Collatz Conjecture". https://www.quantamagazine.org/can-computers-solve-the-collatz-conjecture-20200826/.
- ↑ 7.0 7.1 7.2 Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W. (2016). "Theory and Applications of Satisfiability Testing – SAT 2016: 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings". in Creignou, Nadia; Le Berre, Daniel. 9710. pp. 228–245. doi:10.1007/978-3-319-40970-2_15.
- ↑ 8.0 8.1 Hartnett, Kevin. "Computer Search Settles 90-Year-Old Math Problem". https://www.quantamagazine.org/computer-search-settles-90-year-old-math-problem-20200819/.
 |
