数学論文全体のLean 4形式化（マトロイド理論・Main Theoremまで）

はじめまして。 数学論文の内容を、Lean 4で可能な限り完全に形式化していただける方を探しています。 対象の論文はこちらです。 “A Nine-Element Minor Theorem for 3-Connected Nonbinary Matroids with a W4-Minor” https://figshare.com/articles/preprint/_b_A_Nine-Element_Minor_Theorem_for_3-Connected_Nonbinary_Matroids_with_a_W4-Minor_b_/33689407?file=69305773 分野はマトロイド理論（Matroid Theory）です。 今回お願いしたいのは、一部の定理だけではなく、原則として論文全体のLean化です。 具体的には、 ・論文で使用している定義の形式化 ・前提となるマトロイド理論の定義・補題の整備 ・本文中のLemma、Proposition、Theorem、Corollary等の形式化 ・Main Theoremまでの証明の形式化 ・reduction、minor、deletion、contraction、3-connectivity、binary/nonbinary matroid等、証明に必要な概念の形式化 ・有限場合分けや計算機検証を使用している箇所についても、可能な限りLean内部で検証できる形にすること ・Lean内部だけでの直接計算が現実的でない箇所については、形式的に検証可能なcertificate等を用いる方法の検討 ・最終的にLeanでエラーなくコンパイル・検証できるコード一式の納品 を希望しています。 Lean 4 + mathlibを基本として考えていますが、既存のmathlibのmatroid関連ライブラリを最大限利用していただいて構いません。 重要なのは、単に論文の文章をLean風に書き換えることではなく、最終的にLean kernelによってMain Theoremまでチェックできる形式証明にすることです。 論文中で既存文献の結果を使用している場合についても、 1. mathlib等に既に存在するものを利用する 2. 存在しなければ必要な補題をLeanで証明する 3. 非常に大規模な既存定理が必要になる場合は、どこまで形式化する必要があるか相談する という形を想定しています。 Phase 1：定義・基本ライブラリ Phase 2：主要補題 Phase 3：構造的Reduction Phase 4：有限検証部分 Phase 5：Main Theorem のように段階的に進める方法でも問題ありません。 また、途中成果のLeanコードも随時共有していただきたいです。 最終納品物としては、 ・Leanソースコード一式 ・lakefile等を含む再現可能なプロジェクト ・使用したLean/mathlibのバージョン ・README ・論文の各Lemma/TheoremとLean上の定理との対応表 ・第三者がcloneして `lake build` 等で検証できる状態 を希望しています。 まず、この論文全体をご確認いただいた上で、 ・全文のLean形式化が可能か ・どこが特に難しいと考えられるか ・おおよその費用 ・段階的に依頼する場合の料金 ・納品までの進め方 についてご相談させていただければと思います。 特にマトロイド理論そのものの知識がなくても、Leanによる高度な数学の形式化経験が十分にある方であれば相談したいと考えています。 よろしくお願いいたします。