マリイン・ホイレ

マリーヌス・ヨハネス・ヘンドリクス・ホイレ（1979年3月12日、オランダ、ラインスブルク生まれ）^{[ 1 ] [ 2 ]}は、カーネギーメロン大学のオランダ人コンピュータ科学者で、 SATソルバーを研究している。ホイレはこれらのソルバーを使用して、ブールピタゴラス三つ組問題、シューアの定理第5番、 7次元のケラー予想などの数学的予想を解決した。

ヒューレは2008年にオランダのデルフト工科大学 で博士号を取得した。 2012年から2019年までテキサス大学オースティン校で研究員、後に研究助教授を務めた。 2019年からはカーネギーメロン大学コンピュータサイエンス学科の准教授を務めている。^{[ 2 ]}

2016年5月、彼はオリバー・クルマンとビクター・W・マレクと共に、SATソルビングを用いてブールピタゴラス三つ組問題を解決した。^{[ 3 ] [ 4 ]}彼らが証明した定理の記述は以下の通りである。

この定理を証明するために、{1, ..., 7825} の可能な彩色をヒューリスティックを使用して 1 兆個のサブケースに分割しました。各サブクラスは、ブール充足可能性ソルバーを使用して解決されました。証明の作成には、テキサス先端計算センターの Stampede スーパーコンピュータで 2 日間にわたって約 4 CPU 年分の計算が必要で、200 テラバイトの命題証明が生成されました (使用されたサブケースのリストの形式で 68 ギガバイトに圧縮されました)。^{[ 5 ]}この証明を記述した論文は SAT 2016 会議で発表され、^{[ 5 ]}最優秀論文賞を受賞しました。^{[ 5 ]} 1980 年代にこの問題の解決に対してロナルド グラハムが最初に提供した100 ドルの賞金はHeule に授与されました。^{[ 3 ]}

彼は2017年にSATソルビングを用いて、シュール数5が160であることを証明した。^{[ 4 ] [ 6 ]}彼は2020年に7次元におけるケラー予想を証明した。 ^{[ 7 ]}

2018年、ヒューレとスコット・アーロンソンは、 SATソルビングをコラッツ予想に適用するために、全米科学財団から資金提供を受けた。^{[ 7 ]}

2023年に彼はSubercaseauxと共に、無限正方形グリッドのパッキング彩色数が15であることを証明した。^{[ 8 ] [ 9 ]}

• コンピュータ支援証明#アプリケーション

• 公式サイト
• テキサス大学オースティン校の旧公式サイト