2026-09-25 · article 組合せ幾何エルデシュの問題Lean 4

外接半径の相異なる四点 — n4 = 7

エルデシュ問題集（erdosproblems.com）は、数学者ポール・エルデシュが残した問題を番号付きで集めた Web サイトです。この記事はそのうちの問題 827（以下 #827。https://www.erdosproblems.com/827）を扱います。問いは、平面に点を置いたとき、「4 点の中から 3 点ずつ取って作る四つの三角形の外接半径（三点を通る円の半径）がすべて異なる、そのような 4 点」を必ず含むには何点要るか、というものです。答えは 7 です。この問題は 2026-09-22 に同じサイトのフォーラムで既に解かれています。先行記録の側も、他の人による検証を求めていました。この記事はその後追いで、n4 = 7 の証明を別の道で Lean 4（証明を機械で検査する定理証明支援系）に組み、鎖の全体で機械検査を通した、独立な検証の形です。

Lean機械検査済み（Lean 4、sorry 0・native_decide 不使用、公理は propext・Classical.choice・Quot.sound の部分集合。定理名を添える） 紙証明はあるが機械検査は未了 計算この端末で確かめた範囲。外に出す主張にはしない 既知既知の定理・言い換え・外の文献の確認

このページは nk の増大の速さについては何も主張しません。ここにあるのは k = 4・平面のただ一つの値です。nk の上界・下界の漸近（k が大きいときの振る舞い）は、下の §02 に挙げた既知のものがそのまま最良です。

nk を、次が成り立つ最小の数とする：平面 R2 の nk 点が一般の位置にあれば、その中に k 点の部分集合で、C(k,3) 個の三点組がすべて相異なる半径の円を決めるものが存在する。nk を決定せよ。

エルデシュの問題 #827（原文の言明の訳）。

一般の位置の意味は、この問題ではエルデシュ自身の規約を取ります。既知

この三つ目が効きます。後で述べる上界の証明は「3 点が共線でない」ことを内側で三箇所使っており、共線を許す弱い規約（Martínez と Roldán-Pensado が使うもの）に取り替えると、この記事の鎖からは 7 ≤ n4 ≤ 9 までしか出ません。値は規約に依ります。

k = 4 のときの量を書き下します。4 点 a, b, c, d に対して三角形は 4 個——それぞれ 1 点を除いて作る bcd・acd・abd・abc です。この 4 個の外接半径がどの二つも異なるとき、4 点を良いと呼びます。N 点の集合が一般の位置にあるとき必ず良い 4 点を含むなら N を良い点数と呼び、良い点数の最小が n4 です。逆に、一般の位置にあってどの 4 点部分集合も良くない配置を悪い配置と呼びます。

先に記録した本人が、上界について「Singular・SAT ソルバ・別の問題についての手作業の補題五本に依っている。二度目の実装で全工程を組み直したが、どちらも AI の援用なので独立な査読ではなく自分の再確認にすぎない。誰か他の人に走らせてほしい」と書き添えています。このページの証明は、列挙も反駁も代数もそれとは別の道で、SAT ソルバも数式処理系も使わず、その手作業の補題にも依らずに同じ値へ届き、鎖の全体が Lean の核で検査されています。そこで求められている独立な確認に当たるものです。ただし先の計算の各工程を再実行も監査もしていません——確かめたのは値であって、あちらの計算ではありません。Lean

視点の言い換えとして、「どの三点組も相異なる半径の円を決める集合」を円シドン集合と呼ぶ見方があります。この言い方だと確率的な削除の論法はシドン集合の古典的な議論そのままになり、n 点は ≫ n1/5 の円シドン部分集合を含む、と読めます。既知

Lean での言明はこれです。Lean

theorem sInf_isGood_eq_seven : sInf {N : ℕ | IsGood N} = 7

定義は四つだけで、どれも幾何の言葉をそのまま写したものです。Pt は ℝ × ℝ、sqdist は二点の距離の二乗、cross a b c は符号つき面積の二倍、det4 は四点が一円または一直線に乗ることを表す行列式です。

def GeneralPosition {N : ℕ} (p : Fin N → Pt) : Prop :=
  (∀ i j : Fin N, i < j → p i ≠ p j) ∧
  (∀ i j k : Fin N, i < j → j < k → ¬ Collinear3 (p i) (p j) (p k)) ∧
  (∀ i j k l : Fin N, i < j → j < k → k < l → ¬ Concyclic4 (p i) (p j) (p k) (p l))

def CircumRadiusSq (a b c : Pt) (r : ℝ) : Prop :=
  ∃ o : Pt, sqdist o a = r ∧ sqdist o b = r ∧ sqdist o c = r

def FourDistinct (a b c d : Pt) : Prop :=
  ∀ i j : Fin 4, i ≠ j → ∀ r s : ℝ, face a b c d i r → face a b c d j s → r ≠ s

def IsGood (N : ℕ) : Prop :=
  ∀ p : Fin N → Pt, GeneralPosition p →
    ∃ i j k l : Fin N, i < j ∧ j < k ∧ k < l ∧ FourDistinct (p i) (p j) (p k) (p l)

読むときに確かめる点が四つあります。(1) p は写像ですが GeneralPosition の第一項が単射性を与えるので「相異なる N 点」です。(2) 添字を増加順に取っているので、各部分集合は一度だけ調べられます。(3) 外接半径は二乗で述べられています。半径は非負なので、二乗が相異なることと半径が相異なることは同値です。(4) CircumRadiusSq は存在の形（「中心があって三頂点までの距離の二乗が r」）なので、外接円の存在を仮定に置いていません。一般の位置では三点は共線でないため存在し一意です。

整数座標の 6 点が一つあれば n4 ≥ 7 が出ます。Lean に入っている配置はこれです。Lean

この 6 点は一般の位置にあり、15 通りの 4 点部分集合のどれにも、外接半径の等しい三角形の対があります。有理数の演算だけで確かめられ、Lean の側もそうしています（seven_le_sInf_isGood_and_sInf_isGood_le_nine）。

形

点を (2,3) について並べ替えると、中心対称（ある点 O について、各点の O に関する対称点も集合に入っていること）であることが見えます。

この形を八面体型と呼びます——6 点が 3 組の対に分かれ、各対から 1 点ずつ取る 8 個の「横断三角形」の外接半径がすべて等しい配置です。八面体の 8 枚の面に対応するので、この名前を使っています。Lean での定義：

def OctahedralSix (q : Fin 6 → Pt) : Prop :=
  ∃ (e : Fin 3 → Fin 2 → Fin 6) (r : ℝ),
    Function.Bijective (fun p : Fin 3 × Fin 2 => e p.1 p.2) ∧
    ∀ a b c : Fin 2, CircumRadiusSq (q (e 0 a)) (q (e 1 b)) (q (e 2 c)) r

なぜ悪いのか

6 点を 3 組の対 {±u, ±v, ±w}（中心を原点に置きました）と見ると、4 点部分集合は二通りしかありません。紙

• 対を二つ丸ごと含む場合——たとえば {u, −u, v, −v}。これは中心について対称な平行四辺形で、一本の対角線の両側にある二つの三角形は中心についての点対称で移り合うので合同、したがって外接半径が等しい。
• 対を一つ丸ごと含み、残りの二対から 1 点ずつ取る場合——たとえば {u, −u, v, w}。このとき現れる三角形 u v w と −u v w はどちらも横断三角形なので、八面体型の定義からその外接半径は等しい。

どちらの場合も等半径の対があるので、この 6 点は悪い配置です。したがって 6 点では足りず、n4 ≥ 7。

八面体型はいつ起きるか

点を複素数と見て {±a, ±b, ±c} と書くと、八面体型であることは平方 a2, b2, c2 が一直線上にあることと同値です。同じことを実座標で書けば Σ (a·b)(a×b) = 0（三つの対についての和）。さらに幾何的には、6 点が一つの直角双曲線の上で、中心について 3 組の対点をなすことと言い換えられます。紙

上の格子の配置では a = (2,3), b = (1,1), c = (1,0) で、平方は (−5,12), (0,2), (1,0)——確かに一直線上です。6 点が乗る直角双曲線は x2 + xy − y2 = 1 を (2,3) だけ平行移動したものです。この族は 3 パラメータあり、有理点の実例もいくらでも取れます。

上界のほうは、悪い 6 点配置の形を尽くすのが仕事になります。鎖は五段です。全部が Lean に入っています。Lean

段 1〜3 を合わせると「一般の位置の悪い 6 点は八面体型である」となり（octahedralHypothesis）、段 4・5 と合わせて IsGood 7、すなわち n4 ≤ 7 が出ます。下界と合わせて n4 = 7。

段 4 の芯——外心の和

この段だけは短い恒等式で済みます。半径 R の等しい二つの円が相異なる二点 u, v を通るなら、二つの中心は u v の中点について対称——したがって中心の和は u + v です。読み替えると、辺 u v を共有する二つの三角形の外接半径が等しいとき、その外心（外接円の中心）の和は u + v。八面体型では一つの頂点を通る横断三角形が 4 個あるので、この恒等式を四回使うと点対称が出ます。8 個の横断三角形のうち 6 個しか使いません。Lean

段 5 の形

もし 7 点が悪い配置なら、点を一つずつ落とした七つの 6 点部分集合はどれも悪く、したがって（段 1〜4 により）どれも中心対称です。3 点が共線でない 7 点集合について、これは不可能です。ここが「3 点が共線でない」を使う箇所の一つで、規約を弱めるとこの段が通らなくなります。Lean

枡と証人

6 点の配置で「どこに等半径の対があるか」を記録するために、枡（ます）を使います。枡とは（頂点の対、共有辺）の組で、6 点から二つずつ取る取り方が 15 通り、残りの 4 点から辺を取る取り方が 6 通りなので、枡は 90 個です。枡 ((c,d),(a,b)) が意味するのは「辺 a b を共有する二つの三角形 a b c と a b d」。

この二つの三角形の外接半径が等しいことは、多項式が一つ消えることに書き換えられます。Lean

一般の位置（とくに四点が共円でないこと）のもとで、Ψ = 0 ⟺ 二つの三角形の外接半径が等しい。この Ψ が消える枡を証人と呼び、90 桁のビット列（マスク）で「どの枡が証人か」を表します。配置 p がマスク w を担う（Carries p w）とは、Ψ が消える枡の集合がちょうど w であることです。

Ψ には別の顔もあります——四つの中点 mid(a,b)・mid(a,c)・mid(b,c)・mid(c,d) が共円であることの行列式の、ちょうど 16 倍です。幾何で言えば、c d の中点が三角形 a b c の九点円（三辺の中点を通る円）の上に乗るということです。Lean

悪い配置であることは、証人の言葉で書けます：15 通りの 4 点部分集合のそれぞれに、少なくとも一つ証人がある。逆に、90 桁のマスクが与えられたとき「そのマスクを担う一般の位置の 6 点があるか」を問うのが、次の仕事です。

座標の道 — 根基への所属

いちばん直接的なのは、方程式を書いて解が無いことを見る道です。証人の集合が決まると Ψ = 0 という多項式の等式が並びます。そこに強制される中点の関係を入れて未知数を減らし（中心対称なら 4 個、平行四辺形が一つなら 6 個まで落ちます）、できたイデアル（並んだ多項式から、足し算と多項式倍で作れる式の全体）を、20 個の共線行列式と 15 個の共円行列式で飽和させます。飽和とは「退化した解（3 点が共線・4 点が共円になってしまう解）を割り落とす」操作です。

結果が ⟨1⟩（イデアルが 1 を含み、多項式の全体になること）になれば、複素数の範囲でさえ配置が無いことになります。言い換えれば、1 がイデアルの根基（何乗かするとイデアルに入る多項式の全体）に属することの証明書が出る、ということです。この道で落ちた類が 10 類。

向きの道 — ζij

座標の道は次数が上がると止まります（消去が終わらない類がありました）。そこで角度に持ち替えます。点を複素数と見て、辺 c d に対して

と置くと、Ψ(c,d;a,b) は w(a) と w(b) の外積になり、等半径であることは δcd(a) = δcd(b) と同値になります。つまり証人は「向きが一致する」という一次の条件です。この形にすると、同じ辺についての証人は自動的に推移律を満たし、相補的な二つの証人は「線が平行か直交」を強制する、といった規則が幾何を経由せずに出ます。Lean

実際の非実現の検査では、向きの量を規格化して wij = ζij / ζ01 と取ります。すると枡の条件は wac wad = wbc wbd、共線の条件は wab = wac という乗法的な関係になり、指数を取れば整数格子の上の線形代数になります。格子の単因子（整数行列を対角化したときに現れる対角成分）を計算すると、残る自由度が有限の場合分けに落ちます。この道で落ちた類が 20 類、格子の単因子まで使って落とした類が 4 類です。

最後の 4 類で効いた観察が一つあります。f = ±1 の枝では三つの三角形の半径の比が r2 = r1 r3 という形に縛られ、どれか一つが必ず 1——すなわち共線——になります。だから三角形は一つ調べれば足ります。母数表示を経由せずに済むので、次数が 105 から 13 に落ちました。

段 1（証人集合は 35 類のどれか）は、90 桁のマスクの空間を尽くす仕事です。全部を列挙することはできない（290 通り）ので、探索木（場合分けを枝分かれとして並べた木）を掘ります。

木の節点は「どの枡が証人であると決めたか（pos）／証人でないと決めたか（neg）」の対です。根は何も決めていない状態。節点で使える手は次のとおりです。

木は尽きました：204,890 節点・1,820 本の部分木・取りこぼし 0。開いたままの葉は 0 です。Lean

この木をそのまま Lean に持ち込むために、一本の定理を「手放した節点が片づけば片づく」形に書き、深い節点から順に並べて 73 ファイルに切り、各ファイルが一つ前を import する形にしました。一番下のファイルに theorem censusComplete が入ります。Lean 側の実測は 74 ファイル・合計 15,955 秒、公理の行は 1,842 行すべてが標準の三公理の部分集合でした。

木を尽くすために最後に要ったのは、置換で節点を写す手（上の表の「正規形へ写す」）でした。これが無いと手放した節点が尽きません。証明に新しい幾何は要らず、必要だったのは「四点を名づける順序を変えても『外接半径が重なる』は変わらない」という並べ替え不変性だけです。

名前空間は DistinctCircumradii。sorry は 0、native_decide（証明の一部の計算をコンパイル済みのコードに任せ、核の検査を省く仕組み）は使っていません。したがって検査は Lean の核（証明を最後に確かめる小さな中心部）で閉じ、外部の計算に依存しません。主定理の #print axioms（その定理が依拠する公理を印字する命令）は次の四行です。

'DistinctCircumradii.restUnrealizable'     depends on axioms: [propext, Classical.choice, Quot.sound]
'DistinctCircumradii.octahedralHypothesis' depends on axioms: [propext, Classical.choice, Quot.sound]
'DistinctCircumradii.isGoodSeven'          depends on axioms: [propext, Classical.choice, Quot.sound]
'DistinctCircumradii.sInf_isGood_eq_seven' depends on axioms: [propext, Classical.choice, Quot.sound]

この四行目は鎖の全体に効きます——sInf_isGood_eq_seven は censusComplete を経由して探索木の 74 ファイル全部に依存しているので、この一行が「鎖のどこにも sorry も追加の公理も無い」ことの検査になっています。

ソースの所在

この記事の Lean は、配布物 principia-src.tar.gz（最上位は principia/、Lean 4 v4.33.1 と Mathlib）に入っています。モジュールは Principia.DistinctCircumradii.* の 100 本、主定理は Principia/DistinctCircumradii/Final.lean の DistinctCircumradii.sInf_isGood_eq_seven、公理は propext・Classical.choice・Quot.sound の三つです。配布物の sha256 は 131d8da3426838ca717991bf642551ee8fa5e2656c4952fb1babf050bd175c1b、公理の出力は axioms-principia.txt にあります。

独立な組み直しで取り直したこと

できあがった証明を一度「作った人の環境から切り離して」通し直しました。連結版 25 本と Final を原本から写し（md5 を開始時と終了時に取り、不変であることを確かめた）、olean（Lean が書き出す検査済みの中間ファイル）を一本ずつ作り直して再検査しています。結果は 26 本すべてが返り値 0・標準エラー出力 0 バイト・sorry と native_decide が 0 件、公理の出力は 549 行あってすべて標準三公理の部分集合でした（505 行が三つ、37 行が propext と Quot.sound、7 行が propext のみ）。探索木の 74 本も同じ方式で全本が通っています。Lean

変換の側も機械で確かめてあります。連結版は「同じ土台を各ファイルが写していた」状態を、写しを削って import に置き換えたものです。残した 667 宣言すべてが、元のファイルの同名宣言と、コメントを除いて文字どおり同じであることを別のプログラムが照合しました。名前の衝突で改名したのは補助的な三つの補題だけで、主定理の言明には触れていません。

何を言い、何を言っていないか

Lean に入っているのは証明の鎖の全体です。下界の配置の検算から、探索木の全数性、34 類の非実現、7 点への持ち上げまで、全部が一本の言明の下にあります。有限の中心部だけを機械検査し、残りを紙に置いた前のページ群との違いはここです。

言っていないことは次のとおりです。

• k ≥ 5 については一言も言っていません。この鎖は k = 4 だけを扱い、しかも 90 枡の構造そのものが k = 4 に固有です。
• 平面（ℝ × ℝ）だけです。高次元の類似は扱っていません。
• 一般の位置の規約に依ります。共線を許す規約では、この鎖から出るのは 7 ≤ n4 ≤ 9 までです。
• nk の増大について何も言っていません。既知の上界 O(k5/log k)・下界 k2−o(1) の間の隔たりは、この記事で少しも縮んでいません。
• 証明は人間が読み通せる形にはなっていません。探索木の 204,890 節点は、Lean が読むためのものです。

既知の事実として使ったもの

このページが足すもの

このページの鎖は、冒頭に述べたフォーラムのコメントを参照せずに組まれたもので、道具立ても違います（あちらは SAT と Singular 上の飽和、こちらは Lean の中に閉じた探索木と証明項）。足しているのは次の点です。

先の記録が求めている独立な確認（§02）に、このページは別の道で答えています——列挙・反駁・代数のいずれも別で、SAT ソルバも数式処理系も使わず、その手作業の補題にも依らず、同じ値を機械検査で確かめました。ただし先の計算の各工程は再実行も監査もしていません。一致しているのは値であって、二つの計算が突き合わされたわけではありません。

探した範囲：問題のページとそのフォーラムの全コメント、および上に挙げた文献の書誌。被引用の一覧は引いていません。上の表の行のうち、探した範囲で見当たらないものについても、「既知かもしれない」以上のことは言えません。

• n5 には同じ道が通りません。段 1〜4 に相当する主張——「悪い集合は中心対称」——が k = 5 では偽です。5 点部分集合がすべて等半径の対を持つのに中心対称でない 8 点集合があることが知られています。k = 5 を決めるには別の骨格が要ります。
• 規約の差は埋まっていません。共線を許す規約での n4 は 7 か 8 か 9 のどれかで、この鎖は答えません。上界の証明が「3 点が共線でない」を使う三箇所を、共線の場合も込めて書き直す必要があります。
• 証明が大きすぎます。探索木は 204,890 節点あり、人間が読み通せる形ではありません。悪い 6 点が八面体型であることには、もっと短い理由があるはずです——中心対称性が結論に出てくる以上、対称性を先に出す議論がありそうに見えますが、見つかっていません。
• 独立な第三者の再検査は受けていません。ここに書いた検査は、同じ証明を別の環境で組み直したものであって、別の人が別の道具で確かめたものではありません。Lean のソースは §08 の配布物にあります。

文献