組合せ数学セミナー
発表内容の概要
先ず、グラフの伊原ゼータ関数の定義と行列式表示を述べる。次に、伊原ゼータ関数の
一般化の一つであるweightedゼータ関数について、定義とそれらの行列式表示を与える。
その応用として、離散時間量子ウォークの一つであるGrover walkの時間発展行列(Grover行列)に
関する今野-佐藤の定理を与える。また、今野-佐藤の定理の応用として、Grover/Zeta対応について
述べる。最後に、伊原ゼータ関数の別の一般化であるalternatingゼータ関数を
定式化して、その行列式表示を用いて、Alternating Walk/Zeta対応について触れる。
数理論理学における古典的結果である（各種論理・形式系の）健全性定理・完全性
定理により、様々な設定のもとで、「命題Aの数学的証明の非存在」と、「Aが破れ
ているモデルの存在」とは同値である。これは、組み合わせ論的対象である「証明」
と、代数的対象である「モデル」とを結び付けており、興味深い。では、「命題Aの
長さn以下の証明が存在しない」ことを言うには、どんな対象の「存在」を言えば
よいだろうか？
本講演では、数理論理学の一分野、Proof Complexityにおける重要な考察対象であ
るresolution, Nullstellensatz proof system, Frege systemについて、この観点
から紹介を行い、応用として、（命題論理における）鳩の巣原理の証明の長さにつ
いての知見を概観する。
また、この中でも特にゲームの概念を用いた論法により、（数理論理学内の別分野
である）順序数解析の古典的結果が再解釈できることについても触れたい。
グラフ彩色の研究は、四色定理の研究を起点として発展してきた。四色定理自体
はすでに解決されているものの、グラフ彩色に関連する研究は多くの方向に拡張さ
れている。本講演では、Earth-Moon Problemおよびodd coloringに関する五色問題
を中心に、これらに関連する研究の概観を述べる。その後、biplanar graphのodd
coloringに関して、講演者自身の研究成果を報告する。
フランクルの予想は、組合せ論の長年の未解決問題の一つです。有限台集合上の共通
部分で閉じた集合族で、全体集合と空集合を含むものを考えます。このような集合族
には必ず「rareな頂点」が存在するというのが、フランクルの予想です。「rareな頂
点」とは、その頂点を含むhyperedge(集合族の要素）の個数が、hyperedge全体の個
数の半分以下である頂点を指します。この予想は現在も未解決ですが、いくつかの簡
単なクラスでは成り立つことが知られています。その一つが「Ideal集合族」と呼ばれ
るクラスです。Ideal集合族は、空集合と全体集合を含み、全体集合以外のhyperedge
が部分集合で閉じているという性質を持つ集合族です。Ideal集合族は共通部分でも
閉じていることが容易に確認できます。本発表では、このIdeal集合族に焦点を当て
て議論を進めます。
一方で、頂点全体の平均的な次数がrare（hyperedgeの大きさの合計が、台集合の
大きさとhypereハイパーエッジ数の積の半分以下である場合,つまり
(各hyperedgeの大きさの合計)*2−(台集合の大きさ)*(hyperedge数))<=0））
である集合族が、必ずrareな頂点を持つことは比較的簡単に示すことができます。
今回の研究では、Ideal集合族が平均的にrareであることを証明しました。その後、
形式証明支援システムのLean 4を用いて証明を形式的に記述し、正確性を検証しまし
た。
Lean 4は、数学的な命題や証明を形式的に記述し、その正しさを厳密に保証する
システムです。AIの発達によって、従来は困難であった形式的証明の作成が容易に
なってきました。本発表では、Lean 4の概要についても簡単に解説します。
トップに戻る