1.0/証明開発
命題・証拠・依存関係
数学的結果を構成し、検証し、結び付けます。研究プログラムと独立論文
Crab Research は、数学研究プログラム Proof Engine と、計算機科学・社会科学における独立研究を並列して掲載します。
数学研究プログラム
Proof Engine
Proof Engine は数学的成果、公開された方法論、形式検証を通じて、信頼できる AI 支援数学の実践を進めます。形式検証とは、定理と証明を証明支援系が検査できる精密な形で記述することです。
- 数学的結果の論文
- 38
研究の選読
選読を見る公開問題、完全分類、構成的理論をたどる、研究への入口です。
形式化とは、定理とその証明を、証明支援系が検査できる精密な形で記述することです。
エルデシュ問題 #1212数論
合成数制約付き可視格子グラフの無限路
数論的な制約を満たす無限格子路を構成し、エルデシュの問いに答えるとともに、ある区間のほとんどすべての極限方向を実現します。
この成果を読む構成的逆理論トロピカル数学
対称トロピカル特性多項式の構成的逆理論
どの係数列が対称トロピカル行列から生じるのか。構成的な判定条件が、実現可能性、行列の復元、パラメータ化アルゴリズムを結びます。
この成果を読む最新の数学研究事例
すべての数学的結果（38）Reference-Gated の証明は、明示された引用定理を仮定として後続の推論を検査します。引用定理自体の証明は検証パッケージに含まれていません。
有向木上のアバランチ複体の普遍的実現
ワーキングペーパー · Zenodo
非交差凸包分割の階数計数と辺上点数の不変性
ワーキングペーパー · Zenodo
順序数グラフの分割関係に対する非普遍性の障害
ワーキングペーパー · SSRN
数学研究プログラム以外
独立研究
Proof Engine 以外の論文を、研究分野ごとに整理しています。