Dvir 2008のKakeya下界の式 `dvirBound q n := C(q + n − 1, n)` にq=3, n=2を代入すると6になる（Lean 4でdecideにより計算、axiom-free）。Leanで証明したのは、この式の値の計算だけです。Kakeya集合の大きさがこの値以上であること（Dvirの定理）のLeanでの証明（`dvir_kakeya`）は、現在sorryが残っていて未完成です。
式
dvirBound 3 2 = Nat.choose (3 + 2 − 1) 2 = Nat.choose 4 2 = 6
LaTeX source
\mathrm{dvirBound}(q, n) := \binom{q + n - 1}{n}; \quad \mathrm{dvirBound}(3, 2) = \binom{4}{2} = 6記号表
| 記号 | 意味 | 型 |
|---|---|---|
| dvirBound | Dvir 2008の下界：全次数 ≤ q − 1のn変数多項式空間の次元 | ℕ → ℕ → ℕ |
| q | 有限体Fの位数（本項目では3） | ℕ |
| n | 空間F^nの次元（本項目では2） | ℕ |
| Nat.choose | 二項係数（Lean mathlib） | ℕ → ℕ → ℕ |
走る最小例
Lean 4で `dvirBound_3_2 : dvirBound 3 2 = 6` を `by decide` で証明し、axiom profileを出力。lean-verify.ymlが実行し、検査状態を生成する。
import CollatzRei.KakeyaDvir open CollatzRei.KakeyaDvir #check @dvirBound_3_2 #print axioms dvirBound_3_2
期待される出力：
dvirBound_3_2 : dvirBound 3 2 = 6 'CollatzRei.KakeyaDvir.dvirBound_3_2' does not depend on any axioms
検査状態
S2形式証明済み (axiom-free)
検査の内訳を見る
| 定理 | CollatzRei.KakeyaDvir.dvirBound_3_2 |
| Lean file | CollatzRei/KakeyaDvirAxiomCheck.lean |
| 公理 | (公理なし) |
| 生成元 | gha (GHA run 39175017999) |
| 生成時刻 | 2026-10-18T23:15:15.522Z |
| Lean toolchain | leanprover/lean4:v4.27.0 |
関係項目
- rp.dvir-bound-3-4 — 両者とも同じ下界の式（dvirBound）の具体値を計算した項目（異なる（q, n）＝（3, 2）と（3, 4）） [related_to]
- rp.dvir-bound-5-4 — 両者とも同じ下界の式（dvirBound）の具体値を計算した項目（異なる（q, n）＝（3, 2）と（5, 4）、関連項目はq＝5で体の位数が大きい場合） [related_to]
- rp.homogeneous-vanishing-fn — 本項目は下界の値の計算（dvirBound_3_2）で、関連項目はRei-AIOS側でDvirの証明を分解した5項目の#5（斉次多項式消失、Dvir 2009（JAMS版）証明の構成要素）。同ファイルKakeyaDvir.leanにあり、両者は同じ証明鎖の別要素 [related_to]
出典
- On the size of Kakeya sets in finite fields — Dvir, Z. (2009) URLAMS (Journal of the AMS 22, 2009; preprint 2008)
- The Kakeya problem in finite fields (Terence Tao expository notes) — Tao, T. (2008) URLWayback
- Rei-AIOS Lean 4ファイル：CollatzRei/KakeyaDvir.lean — Fujimoto, N. (2026) AGPL-3.0 + Commercial
書き手と承認
| 下書き | Claude（AnthropicのAI）2026-10-13 |
| 独立レビュー | Claude（独立レビュー） (2026-10-14) |
| 公開承認 | 藤本 伸樹2026-10-14 |
| ページ生成 | ボット（項目データから自動生成） |
訂正記録 (3件)
C5-corr-001
誤りの種類：主張の範囲の言い過ぎ
何が誤りだったか：name.ja 「Dvir Kakeya 下界 bound(3, 2) = 6」 + summary.ja 「具体 case: ... decide 証明、 axiom-free」 + relations[0].note 「axiom profile 対象 定理」 — Lean で axiom-free に 示して いる の は 「二項係数 の 値 計算 C(4, 2) = 6」 だけ で、 「F₃² の Kakeya 集合 は 6 点 以上」 と いう Dvir の 定理 内容 (= dvir_kakeya、 S0 sorryAx 残) は 示して い ない。 本 書き方 は 「axiom-free」 の 範囲 が 「Dvir の 定理 全体」 と 誤読 される
どう直したか：name.ja を 「Dvir の 下界 の 式 の 値: C(q+n−1, n) で q=3, n=2 の と き 6 (計算)」 に 変更 (= 題名 で 「計算」 を 明示)、 summary.ja を 「下界 の 式 ... decide に より 計算、 axiom-free」 + 末尾 に 2 文 追加 (= 「Lean で 証明 した の は 式 の 値 の 計算 だけ」 + 「Kakeya 集合 の 大きさ (dvir_kakeya) は sorry 残 で 未完成」)、 relations[0].note を 「両者 と も Lean 4 CollatzRei project 内 で axiom profile を 検査 した 定理 (別分野)。 同じ ファイル に は sorry が 残る 定理 も ある」 に 変更
発見: Claude（独立レビュー） ｜ 訂正 commit:
d612b7da4C5-corr-002
誤りの種類：出典の不一致
何が誤りだったか：sources[1] (Tao blog) の license を 「Tao's blog (CC-BY-NC)」 と 書いた が、 2026-10-14 WebFetch (= https://terrytao.wordpress.com/about/) で blog 上 に CC-BY-NC を 含む CC 系 license の 明示 が 確認 でき なかった (= 「出典 の license 記述」 が 出典 の 実態 と 一致 し ない)
どう直したか：sources[1].license を 「Tao's blog (CC-BY-NC)」 → null、 新 field license_note に 「未確認 (2026-10-14 Tao blog about page に Copyright etc. section あり、 reasonable portions の copy/quote/translate 許可 の custom policy、 CC-BY-NC を 含む CC 系 license の 明示 なし)」 を 追記
発見: Claude（独立レビュー） ｜ 訂正 commit:
d612b7da4C5-corr-003
誤りの種類：出典の不一致
何が誤りだったか：走る最小例の期待出力を、Leanを実際に走らせずに書いていた。実際に走る最小例をLeanで実行すると、`open CollatzRei.KakeyaDvir` の影響で短い名前（dvirBound_3_2）で表示されるが、以前の期待出力では完全な名前（@CollatzRei.KakeyaDvir.dvirBound_3_2）で書いていた。定理の内容、必要な公理（なし＝axiom-free）、検査状態の表示は実機の出力と一致している（表示の仕方だけが違っていた）。
どう直したか：走る最小例の期待出力を、実際にLeanで実行した結果に合わせて直しました。以前の期待出力は実行せずに書いたもので、定理名の表示の仕方（完全な名前か短い名前か）が実際の出力と違っていました。定理の内容、必要な公理、検査状態の表示は変わっていません。
発見: 藤本 伸樹 ｜ 訂正 commit:
2dfb14ea15c1bab822e4cee7badb2bac00925564全項目の訂正一覧: /reipedia/corrections/