対称トロピカル特性係数データに対する構成的な逆判定条件と同じ次数での再構成を与え、欠損項と任意の Newton 多角形を扱う。孤立ギャップの実現と Kiani–Tavakolipour 予想 6.1 の全次元での証明も与える。Lean 付属資料は明示された数学的命題を検証する。アルゴリズムとビット計算量に関する主張については、論文全体と形式化の対応を再審査している。

SSRN2026-09-15 Zenodo2026-09-02 形式化

2026-08-25

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

パターン回避 Canon 順列の剛性・降下・Wilf 分類

Canon 順列の剛性、降下公式、大域的 Wilf 分類を研究する。現在の公開原稿は、完成した形式化パッケージより前の版である。

Zenodo2026-08-25

2026-09-05改訂 2026-09-18

組合せ論 Kernel-Onlyワーキングペーパー · Zenodo

155 通りのルーク配置を持つ順列格子

完全なルーク配置がちょうど 155 通りとなる順列格子を構成して Lewis–Won 予想 3.10 を否定し、8 以上のすべての次数に反例を与える。

Zenodo2026-09-11 Kernel-Only の形式化

2026-08-25

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

端点反復 Canon 順列：錐内歩行とスペクトル幾何

錐内歩行の解析的な関連論文として、確率・調和・スペクトル幾何を扱う。論文全体の形式検証は進行中。

Zenodo2026-08-25

2026-03-11改訂 2026-09-08

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

x + by = bz の Rado 数：b^k パターンと閾値予想

方程式 x + by = bz に対し、R_k(b) はどの k 色彩色にも単色解が存在する最小の区間サイズである。本論文は既知の各場合の解析的証明、有限の充足可能性（SAT）検査、および R_5(3) が 296 を超えることを示す明示的な5色彩色を与える。閾値予想は R_k(b) が b^k に等しくなる条件を記述するが、一般の予想は未解決である。2026年9月の訂正では、既知の下界 R_5(2) ≥ 56 が Chang、De Loera、Wesley の R_4(2) = 56 から従うことを明記した。Lean による形式化は部分的であり、証明全体が Lean のカーネルで検査されたわけではない。

SSRN2026-06-03 Zenodo2026-03-11 コードと資料

2026-05-22

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

Rado 方程式 x + by = bz の距離対特徴付け：Lean 4 のカーネルのみを用いた形式化

対応する Rado 閾値の一方向を支える距離対の仕組みを Lean で形式化し、解析的カスケードの仮定を明示的に残す。

Zenodo2026-05-22 コードと資料

2026-07-12改訂 2026-08-31

組合せ論 Kernel-Onlyワーキングペーパー · SSRN

非交差分割の細分グラフにおける Hamilton 閉路と道

非交差分割の細分グラフにおける Hamilton 閉路と道を完全分類し、統一的な構成と偶奇による障害を与える。

SSRN Zenodo2026-07-12 Kernel-Only の形式化

2026-09-06改訂 2026-09-14

数論 Kernel-Onlyワーキングペーパー · SSRN

合成数制約付き可視格子グラフの無限路

頂点は両座標が一より大きい互いに素な整数対で、各頂点の少なくとも一方の座標は合成数とする。隣接頂点は単位歩で結ばれる。論文は無限路を構成し、区間 (4/3,5/3) のほとんどすべての比について、その比を極限座標比とする無限単純路を与える。改訂稿は rafalwrona の局所的な行列式の観察と、Duncan の有限路の観察を引用する。証明はさらに、小さい素因子を持たない合成数の短い帯、安全な支持列、方向を同時に制御する評価、およびスケール間の接続を与えて、大域的な定理に到達する。

SSRN2026-09-14 Zenodo2026-09-06 Kernel-Only の形式化

2026-09-06改訂 2026-09-18

組合せ論 Kernel-Onlyワーキングペーパー · SSRN

加法的な増大ギャップは対数凹性を保証しない

独立集合を拡張する規則を一定の加法的余裕だけ緩めても、サイズ別の独立集合数の対数凹性は保証されない。13 元集合上のランク 4 の例は個数列 1, 13, 25, 7, 2 をもち、Xie と Xu のランク依存の予想に反例を与える。さらに、同じ増大パラメータを保ちながら対数凹性の比が 0 に近づく族を構成する。

SSRN2026-09-14 Zenodo2026-09-06 Kernel-Only の形式化

2026-09-06

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

任意の次数の実根近傍多項式

近傍多項式は共通の隣接頂点をもつ頂点部分集合を大きさ別に数える。任意の最大次数に対し、その近傍多項式が相異なる負の実根のみをもつ木を構成して Day の問題を解決し、最大次数を固定した係数極限を完全に特徴づける。

Zenodo2026-09-06

2026-09-06改訂 2026-09-17

組合せ論 Kernel-Onlyワーキングペーパー · Zenodo

非負な円分多項式の積と面数が平方数のサイコロ

円分多項式は原始的な1の冪根を零点にもつ。異なる二つの素数の冪で定まる積の族について、係数がすべて非負となる場合を完全に分類し、面数が平方数のサイコロの付け替えに関する Fiore–Nasr–Stone 予想5.7を解決する。乗数の次数の最良下界とすべての等号成立条件も証明する。論文の数学的結果には、通常の整数係数多項式を用いた公開の Lean 4 証明がある。

Zenodo2026-09-06 Kernel-Only の形式化

2026-09-06

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

二項係数の冪和の比の最大値とガウス極限

二項係数の重み付き冪和を途中で切った部分和と、より短い行の全体和の比を研究する。正の実数冪と正の重みを固定して、予想された最大値の漸近式、補正された整数上の最大位置、ガウス極限を示す。二乗の場合は、すべての正の重みで狭義の対数凹性も示す。

Zenodo2026-09-06

2026-09-06改訂 2026-09-18

組合せ論 Kernel-Onlyワーキングペーパー · Zenodo

独立集合のしきい値ゲームと奇数長の閉路上の測地的除去

測地的除去ゲームは、未選択の頂点に最短路を繰り返し加えても固定された元のグラフ全体を生成できなくなると終了する。頂点数が五以上の奇数長の閉路では、選択済み集合が終端となるための必要十分条件は、巡回順序を変えて得た閉路の最大独立集合を含むことである。この対応から動的なペアリング戦略による後手必勝と正確な勝利手数が得られ、パスと閉路上の独立集合しきい値ゲームへ拡張される。

Zenodo2026-09-06 Kernel-Only の形式化コードと資料

2026-09-06改訂 2026-09-18

組合せ論 Kernel-Onlyワーキングペーパー · Zenodo

円柱グラフの四部分多重集合識別分割

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

Zenodo2026-09-06 Kernel-Only の形式化コードと資料

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改訂 2026-09-08

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

占有数が有界なトークングラフのマッチングと独立数：独立に進められた開発

区別できない一定個数のトークンをグラフの頂点に配置し、一回の移動で一つのトークンを一辺に沿って動かす。本稿は Reyes、Dalfó、Fiol の予想3.6について独立に得た証明と、占有数が有界な場合の帰結を記録する。Patel が先に公開した完全解答は、占有数が無制限の場合を同じ基本構成で解いている。各マッチング辺のトークン総数を固定し、道の直積上でマッチングを構成する方法である。改訂稿は独立に進められた研究の解説として保存し、最初の解答としての優先権を主張しない。

Zenodo2026-09-06

2026-09-07

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

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

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

Zenodo2026-09-07

2026-09-07改訂 2026-09-28

組合せ論 Kernel-Onlyワーキングペーパー · Zenodo

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

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

Zenodo2026-09-07 Kernel-Only の形式化

2026-09-07

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

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

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

Zenodo2026-09-07

2026-09-07

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

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

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

Zenodo2026-09-07

2026-09-07

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

単射な制限がすべて偶となる変換

有限順序集合上の写像について、逆転とは二つの入力の像が逆の順序に並ぶことである。本論文は、像が互いに異なる t 個の入力をどう選んでも逆転数が偶数となる写像を分類する。同じ像を持つ入力が一つのブロックを成し、ブロック数を階数と呼ぶ。得られるブロック条件は、Vítor H. Fernandes が arXiv 2605.12342 で提起した、階数 t と t+1 に関する二つの未解決の場合に答える。これらの写像と、二度作用させても一度の作用と同じになる写像について閉じた計数公式を与え、部分的に定義された写像および逆転数が奇数となる制限にも分類を拡張する。

Zenodo2026-09-07

2026-09-08改訂 2026-10-02

組合せ論 Kernel-Onlyワーキングペーパー · Zenodo

隣接値の差が有界な 132 回避置換の厳密な増大と降下の閾値

三つの要素が相対的な大小関係 132 の順に現れない置換を、132 回避置換という。隣接する値の差の絶対値を m 以下に制限した族の指数増大率は、m とともに厳密に増加する。これは Mayama と Akita の数え上げ理論に基づき、Nadler の予想 2 に残された主張を証明する。要素が直後の要素より大きい位置を降下と呼ぶ。各降下に重みを与えると、増大率が一となる領域と、異なる二つの閾値スケールが現れる。本論文は重み付き増大の判定条件と極限増大率も一つの論文にまとめて証明する。

Zenodo2026-09-08 Kernel-Only の形式化コードと資料

2026-09-08

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

色付き交錯三角形の鋭い安定化閾値と固定エネルギーの法則

深さ二の色付き交錯三角形では、各色が上段に二回、下段に一回、上・下・上の順に現れる。Patel の先行する完全解答は、Blitvić–Petrov モデルの係数が最終的に多項式となることと、キュムラントの線形性を証明している。本稿は同じ機構を精密化し、任意の固定次数 k での最適な閾値 n が2k+1以上となること、厳密な境界差、逆転数を記録した極限法則および空間的極限法則を示す。下段が恒等順序なら最適な閾値は n がk+1以上に改善される。重複する低次数の導出は除いた。大域的対数凹性の予想4.1は対象外である。

Zenodo2026-09-08

2026-09-08

位相幾何学内部レビュー完了ワーキングペーパー · Zenodo

二橋結び目の符号数の厳密な分散と精密な極限定理

二橋結び目は二つの上橋を持つ図で表せ、その符号数は整数値の結び目不変量である。Cohen、Baker、Dam、Felber、Madras、Saha、Thackrah が用いた語のモデルでは、一部の結び目が二度数えられる。本論文は各交点数 c における符号数の厳密な分散を求め、分散から c を引いた値が -14/3 に収束することを証明し、arXiv 2604.21107 の数値的予想 5.1 に答える。また、個々の符号数の確率と、まれに現れる大きな符号数の確率について、より高精度な近似を与える。鏡像同士を同一視した結び目の類を一様に選び、正負を独立かつ等確率で選ぶと、別の対称モデルが得られる。正確な標本抽出の重みを保ち、このモデルの分散と確率の補正が交点数の偶奇によってどう変わるかを導く。

Zenodo2026-09-08

2026-09-08改訂 2026-10-11

解析と確率 Kernel-Onlyワーキングペーパー · Zenodo

指数エネルギーの厳密な配置と衝突スケール

重複を許して区間に点を配置し、各点対の距離 d に対する exp(-d) の和を最小にする。本論文は最小配置の全位置と各端点に重なる点の正確な個数を求める。単位区間では、Emmerich が arXiv 2603.28179v2 の第4節で報告した経験的な三分の一則を証明する。また、点数と区間長を固定して、付録 A.3 末尾の近傍の q に関する問いに答える。exp(-d^q) で q が下から1に近づくと、端点群の動く点は異なる指数スケールで端点に近づく。特別な区間長では、最外層は対数補正を伴う別のスケールになる。q が上から1に近づく場合は、これらの長さも含めて端点の重複度が保たれる。有限サイズのエネルギー補正と指数スケールに共通する主要因子も、一つの論文で証明する。予想 A.1 と A.2 の大域的転移は、この局所結果の対象外である。

Zenodo2026-09-08 Kernel-Only の形式化

2026-09-09改訂 2026-09-10

集合論 Reference-Gated · 中間公開版ワーキングペーパー · SSRN

順序数グラフの分割関係に対する非普遍性の障害

Erdős 第597問は、順序数の平方 ω₁² の2彩色にどのグラフが必ず現れるかを問う。本稿は Shelah の既知の非普遍性定理を、Erdős が報告した Baumgartner の負の分割関係に適用し、対象を有限グラフに限定しない主張に反例を与える。対象はちょうど ℵ₁ 個の頂点を持つ連結二部グラフで、直径は3以下、可算無限完全二部グラフを含まない。完全二部部分グラフの明示的なランク証明と連結な対象の構成を示し、木の節点の比較可能性を使う先行手法を Shelah に帰属させる。Lean の付随コードは構成と引用した Baumgartner の定理からの導出を検証し、その引用定理の証明自体はコードベースの範囲外にある。Reference-Gated はこの機械検証の境界を表す。有限対象の問いは未解決のままである。

SSRN2026-09-10 Zenodo2026-09-09 Reference-Gated の形式化コードと資料参照関門：命題と出典

2026-09-09

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

非交差凸包分割の階数計数と辺上点数の不変性

凸多角形の境界上の有限個の点を、異なるブロックの凸包が互いに交わらないように分割する。階数は点の総数からブロック数を引いた値である。本論文は各階数の分割数を求め、各辺の内部点数を任意に並べ替えても、これらの数が変わらないことを証明する。すべての辺に内部点がある場合、各階数の分割数から辺の内部点数とその重複度も復元できる。出発点となった Dougherty–Root の多角形配置に関する非階数対称性予想と相反恒等式は、すでに Shivam Patel が証明している。本論文の新しい寄与は全階数の計数と任意の辺点数の置換に対する不変性である。共線配置は対象外である。完全な証明を含むが、形式化はまだ行っていない。

Zenodo2026-09-09 コードと資料

2026-09-09

位相幾何学内部レビュー完了ワーキングペーパー · Zenodo

有向木上のアバランチ複体の普遍的実現

並列チップ発火過程で同時に発火する頂点集合が生成する単体複体を、アバランチ複体という。各頂点の初期チップ数を零または一とし、唯一の吸収点に向かう木の上で、頂点を持つ任意の有限単体複体を誘導部分複体として実現する。明示的な単体崩壊により補助頂点を除き、目標のホモトピー型を保つ。これにより Riihimäki–Smith の第 5 節の問題 2 を有限個の球面のウェッジについて解き、続くねじれと非ウェッジの問いにも答える。整合的なレトラクションにより、空でない有限フィルトレーションも時間の細分と標本化の後に実現できる。別の固定有向路の予想 3.11 は対象外である。完全な数学的証明を与えるが、証明支援系での形式化は未実施である。

Zenodo2026-09-09 コードと資料

2026-09-09改訂 2026-09-10

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

固定重みネックレスの逆余辞書式普遍サイクル

巡回移動だけが異なる語を一つのネックレスとみなす。長さと各桁の和が固定された非負整数の語について、最後の一桁を除いた各許容語がちょうど一度現れる循環列を構成する。Campbell–Janik-Jones–Sawada の予想 8、すなわち末尾から比較する逆余辞書式順序で各ネックレスの最短反復ブロックを連結すると、指定された欠落記号の後続規則によるサイクルが得られることを証明する。一記号あたりの償却時間は定数で、補助記憶領域は語の長さに比例する。この証明は、最初の正の座標から次の座標へ一単位を移す操作で閉じた族にも適用でき、標準代表の接頭辞和に制限を課す場合も含む。完全な数学的証明を与えるが、形式化は未実施である。

Zenodo2026-09-10 コードと資料

信頼性と検証の基準

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

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

Paper Close は、公開前に準備と内部レビューを終え、ワーキングペーパーとして公開したことを示します。通常の学術プレプリントとしてお読みいただき、議論してください。今後の検証や議論によって修正が必要になる場合があります。完全な形式化や外部査読を意味するものではありません。

引用定理を用いた機械検証（Reference-Gated）

コードは出典を明示した引用定理の命題を入力として、その後の導出を検証します。引用定理自体の証明は現在の検証パッケージの範囲外であり、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 支援数学では、論証の候補を、検査済みで読みやすく保守可能な成果へとつなぐ、明示的な工学的基盤がますます重要になると考えます。Proof Engine 研究プログラムは、信頼できる数学的成果の生産と、成果を解釈して概念や新たな方向を生み出す構造研究という、相互に協力する二つの役割を探究します。これらの役割は重なり得て、AI は双方を支援できます。専門の数学者は、より深い構造理解において引き続き中心的な役割を担います。公開問題は、再利用可能な数学的貢献の出発点です。本プログラムは、実際の成果、主張の証拠、その後の再利用と訂正の実践を通じて評価されます。詳しくは研究プログラムをご覧ください。

方法論

Proof Engine 1.0 と 2.0

Proof Engine は、信頼できる AI 支援数学の研究プログラムです。公開済みの二つの方法論は相互に補完します。1.0 は証明開発を組織し、2.0 は研究過程を統括して、その中で 1.0 を利用できます。研究プログラムと公開の責務を読む

Proof Engine 1.0

証明開発

正確な命題・証拠・依存関係を組織し、未解決の証明義務を明示し、訂正を論証全体へ伝播させます。

論文を読む · SSRN 7237460

初回公開: 2026-07-29
最新の公開改訂: 2026-08-31

Proof Engine 2.0

研究ガバナンス

数学的探究の問い、意図する貢献、必要な証拠を統括します。自律的な実行は、人間が承認した範囲内に留まります。

論文を読む · Zenodo ワーキングペーパー

初回公開: 2026-09-05
最新の公開改訂: 2026-09-05

方法論の論文 6

並べ替え

SSRN のワーキングペーパーは、十分に展開された研究です。一部は意図的に独立したワーキングペーパーとして維持されます。研究の成熟度と公刊状況は別に記録します。

6 件の論文 · 初回公開：新しい順 · 記録更新 2026-10-11

2026-09-08改訂 2026-09-14

数学の研究方法ワーキングペーパー · SSRN

Proof Engine 研究プログラム：信頼できる AI 支援数学と責任ある研究

信頼できる AI 支援数学の研究プログラムとして、公開と訂正の責務、責任ある著者表示、数学的成果の生産と構造研究の相互作用を明確にする。

SSRN2026-09-14 Zenodo2026-09-08

2026-09-08改訂 2026-09-15

数学の研究方法ワーキングペーパー · SSRN

Theorem Notary：カーネル検証済み定理の公開と再利用のための Glass Box プロトコル

Theorem Notary は、定理の正確な記述を通じた再利用を可能にし、その完全な証明、定義、依存関係、基礎公理を引き続き公開して、調査と検証に供する。これが Glass Box（ガラスの箱）という設計である。証明書はこれらの資料を結び付け、署名は供給者を示す。プロジェクトは新しい結果を導出して公開するときにも、有効な検証結果を保持する。

SSRN2026-09-15 Zenodo2026-09-08 形式化コードと資料

2026-09-05

数学の研究方法ワーキングペーパー · Zenodo