頂点から各分割部分への最小距離を、部分のラベルを捨て、重複を保って記録する。同じ長さの二つの閉路の対応する頂点を結んだプリズムグラフでは、閉路長が十以上なら四部分で全頂点を識別でき、この数が最適である。閉路上の距離の明示式により、指定した円柱グラフの分割について正確な高さの限界も求める。閉路長が八または九のプリズム、および層数が二以上で偶数周長が十二以上の円柱グラフには五部分の上界を与える。

Zenodo2026-09-06

2026-09-06

組合せ論内部レビュー完了ワーキングペーパー · Zenodo

完全なルーク配置は、各行と各列の極大な連続白マス区間からちょうど一つのマスを選ぶ。黒マスを k 個一様に選ぶ n×n 盤では、k が n の平方根より遅く増加するとき、配置数の平均は n!(n/36)^k に漸近する。k/sqrt(n) が有限値 lambda に近づくと、正規化した平均は exp(-27 lambda^2/50) に近づく。連結成分の解析から、盤と配置の組を一様に選んだ場合の空間分布と、一様な盤に配置が存在する確率の評価も得られる。

Zenodo2026-09-06

2026-09-06

組合せ論内部レビュー完了ワーキングペーパー · Zenodo

占有数に上限のあるトークングラフのマッチングと独立数

構成は一定数の区別できないトークンをグラフの頂点に配置し、一回の移動で一つのトークンを一本の辺に沿って動かす。占有数が無制限、または共通の上限が偶数の場合、二部底グラフの一方の部を端点の重ならない辺で覆えるなら、その部の占有総数が偶数の構成全体は最大独立集合となる。すなわち、一回の合法な移動で互いに結ばれず、この性質を持つより大きな構成集合は存在しない。これによりスーパートークングラフの独立数予想を証明する。頂点ごとに容量が異なる場合の十分条件と、奇数容量での明示的な反例も与える。

Zenodo2026-09-06

2026-09-07

組合せ論内部レビュー完了ワーキングペーパー · Zenodo

安定な連続パターンと鎖クラスター

連続置換パターンは、相異なる隣接文字からなるブロックの相対順序を指定する。文字ごとの個数を入れ替えてもパターンの出現回数分布が変わらない場合を特徴づける。その条件は、重なりによって連結した出現の各集まりが、位置全体に一つの全順序を強制することである。語長の上限が最良となる有限の出現対計数テスト、12435 などの非単調な安定例、出現位置集合への拡張と、同長で最小文字から始まるパターン族の同時分布の判定を与える。

Zenodo2026-09-07

2026-09-07

組合せ論内部レビュー完了ワーキングペーパー · Zenodo

接続構造からの再帰的デザインの識別

ここでいうデザインは、ブロックと呼ぶ、相異なる同じ大きさの点部分集合からなる。各ブロックは少なくとも二点を含み、各点は同じ正の個数のブロックに属する。二つの再帰的構成について、点とブロックの所属関係だけから隠れた部分を復元し、ブロックを保つ点の置換、すなわち自己同型をすべて決定する。これにより Amarra、Devillers、Praeger の二つの予想を証明し、例外を分類する。所属ベクトル間の整数関係からは、パラメータを事前に知らずに単一分割構成の入力デザインも復元できる。固定された有限の構成手順列にも、群と同型に関する結果が引き継がれる。

Zenodo2026-09-07

2026-09-07

解析と確率内部レビュー完了ワーキングペーパー · Zenodo

切断 Stieltjes 積分方程の一意なピーク

本論文は積分方程によって定まる曲線を扱う。一つのピークまで増加し、その後減少する正の形状関数 h について、減少側の相対的な傾き xh'(x)/h(x) が狭義減少すれば、存在する各曲線のピークは一意となる。これにより Viakhirev の一意性予想を証明する。積分核のすべての正のべきについて、曲線が存在する水準の正確な範囲とピークの移動を決定する。原論文で提案された正規化対数正規切断では、ピークの位置と高さは切断指数に依存しない極限へ収束し、明示的な一次補正を持つ。一方、ピークが一つだけの滑らかな形状関数でも、導関数がゼロとなる停留点が任意に多い曲線を生じ得る。

Zenodo2026-09-07

2026-09-07

組合せ論内部レビュー完了ワーキングペーパー · Zenodo

頂点ラベル付きグラフの零距離同値類

連結グラフの頂点に非負の数を付け、二点を結ぶ各経路上の最大値について、全経路にわたる下限を取ると距離が定まる。異なる頂点間でも距離がゼロになり得る。この距離で互いに区別できない頂点の集合が零距離同値類である。本論文は指定した集合がこのような同値類となる条件を与える。Dovgoshey と Rovenska の閉路予想を有限同値類の場合に証明し、既知の半 Farey グラフの各辺に新しい頂点を一つ挿入することで、制限のない予想には反例を与える。この反例では、任意の二点間で内部頂点が互いに重ならない経路は高々三本であり、三は可能な最小の一様上界である。さらに、各辺の少なくとも一端に正の値を付けるすべてのラベル付けについて、異なる頂点が分離されるグラフと、各点が孤立点になるグラフを特徴付ける。

Zenodo2026-09-07

信頼性と検証の基準

形式検証とは、定理と証明を証明支援系が検査できる厳密な形で記述することです。以下では、完了した検査と残っている前提を説明します。

内部レビュー済みの原稿（Paper Close）

内部レビューを終えて公開しています。主要結論の完全な形式化はまだ確立されておらず、誤りが残る可能性があります。

外部定理を前提とする検証（Reference-Gated）

引用する定理の一部を明示的な前提とし、証明支援系はその前提の下で残りの推論を検査します。前提とした定理の証明は、まだ公開パッケージに含まれていません。

基礎公理のみに基づく検証（Kernel-Only）

証明支援系は引用結果を含むすべての定理依存を検査し、未証明の定理を追加の前提にしません。許容するのは、推論の出発点となる以下の基礎公理のみです。形式化と論文の対応も確認しますが、説明の修正が必要な場合はあります。

propext (命題の外延性); Classical.choice (古典選択公理); Quot.sound (商型の健全性).

査読済み · 採択済み

独立した査読を経て、学術誌または査読付き会議に採択されています。外部の学術的な受容を示し、採択と正式な公刊は別々に記録します。

最終的な形式化として認める基準は Kernel-Only のみです。Reference-Gated は信頼性がそれより低く、工程規模が特に大きい場合に限って中間版として公開します。査読によって未証明の定理の前提が解消されるわけではありません。

検証方法と適用範囲の詳細を読む

正確な定理依存関係

引用する結果には、正確な定理文、出典、対応する検証済み形式的定理が必要です。Lean/mathlib の既存のカーネル検証済み証明は再利用できます。すべての依存は最終的に propext、Classical.choice、Quot.sound のみに帰着させ、追加の定理公理、sorry、カーネル未検証のネイティブ計算による省略は認めません。

Reference-Gated 版では、正確な命題・仮定・量化・出典箇所・形式的前提・依存する結論を記した関門一覧を公開する必要があります。Kernel-Only に到達するには、検証済み証明ですべての関門を解消し、最終定理と論文との対応を再確認します。

最終定理の公理レポートは、証明が実際に何に依存しているかを示します。その命題が意図した数学的定理に対応するかは別途確認が必要であり、公理レポートだけではその対応は確立しません。

私たちは、AI 時代の数学における重要な変化は成果の量の増加にとどまらず、高速な生成によって、従来の数学体系で検証・解釈・再利用・保守を結ぶ工学的な層の不足が顕在化し、新しい研究の分業が開かれることにあると考えます。AI は論証の候補生成や証明経路の探索に参加し、数学エンジニアのような新たな役割は、それらを検査・再現・継続利用できる成果に整えます。数学者は、価値ある問いを立て、構造を発見し、概念を生み出し、結果を説明・一般化する中心的な役割を担います。これらの役割は重なり得るものであり、Proof Engine は公開された数学的事例を通じて、その基本的な実現可能性を探っています。詳しい論証は方法論論文をご覧ください。

方法論