Back to Problems
kummer_vandiver
Specification
Kummer–Vandiver conjecture states that for every prime $p$, the class number of the maximal real subfield of $\mathbb{Q}(\zeta_p)$ is not divisible by $p$. -
Lean 4 Statement
theorem kummer_vandiver (p : ℕ+) (hp : p.Prime) :
¬ ↑p ∣ (classNumber (maximalRealSubfield (CyclotomicField p ℚ)))
Browse
All Problems
Explore all 300 unsolved conjectures.
View problems →
Docs
Verification Pipeline
How zero-trust verification works.
Read docs →
Evaluation Results
Recent Submissions
| Model | Status | Goals Left | Submitted | Lean Snippet | Output |
|---|---|---|---|---|---|
| GPT-5.3 Codex Agent v8 | Failed | -- | Feb 25, 2026 |
View{
"agent_telemetry": {
"compilations": 0,
"iterations": 10,
"duration_s": 36.14,
"best_status": "pending",
"best_goals": null,
"max_iterations": 10,
"model": "openai/gpt-5.3-codex",
"error": null,
"provider": "openrouter_primary",
"finish_reason": "tool_calls",
"usage": {
"prompt_tokens": 24711,
"completion_tokens": 1466,
"total_tokens": 26177,
"reasoning_tokens": 1214,
"cost_usd": 0.03735865
},
"reasoning_effort": "high",
"response_trace_count": 10
},
"response_trace": [
{
"iteration": 1,
"event": "search_mathlib",
"query": "kummer_vandiver",
"results_count": 0
},
{
"iteration": 2,
"event": "search_mathlib",
"query": "classNumber",
"results_count": 7
},
{
"iteration": 3,
"event": "search_mathlib",
"query": "maximalRealSubfield",
"results_count": 7
},
{
"iteration": 4,
"event": "search_mathlib",
"query": "CyclotomicField p \u211a",
"results_count": 0
},
{
"iteration": 5,
"event": "search_mathlib",
"query": "Prime.not_dvd_one",
"results_count": 1
},
{
"iteration": 6,
"event": "search_mathlib",
"query": "classNumber_eq_one",
"results_count": 8
},
{
"iteration": 7,
"event": "search_mathlib",
"query": "Vandiver",
"results_count": 0
},
{
"iteration": 8,
"event": "search_mathlib",
"query": "isCyclotomic classNumber",
"results_count": 0
},
{
"iteration": 9,
"event": "search_mathlib",
"query": "Cyclotomic classNumber",
"results_count": 0
},
{
"iteration": 10,
"event": "search_mathlib",
"query": "maximalRealSubfield (CyclotomicField",
"results_count": 0
}
]
}
|
|
| Gemini 3.1 Pro Agent v8 | Failed | -- | Feb 24, 2026 |
View{
"agent_telemetry": {
"compilations": 0,
"iterations": 0,
"duration_s": 0.05,
"best_status": "pending",
"best_goals": null,
"max_iterations": 10,
"model": "google/gemini-3.1-pro-preview",
"error": "OpenRouter API error 402: {\"error\":{\"message\":\"This request requires more credits, or fewer max_tokens. You requested up to 65536 tokens, but can only afford 58661. To increase, visit https://openrouter.ai/settings/keys and create a key with a higher total limit\",\"code\":402,\"metadata\":{\"provider_name\":null}},\"user_id\":\"user_2zsm3L1zzBL2yxyrvmrXwgeTimc\"}",
"provider": "openrouter_primary",
"finish_reason": "",
"usage": {
"prompt_tokens": 0,
"completion_tokens": 0,
"total_tokens": 0,
"reasoning_tokens": null,
"cost_usd": 0.0
},
"reasoning_effort": "high",
"response_trace_count": 0
},
"response_trace": []
}
|
|
| Gemini 3 Flash Agent v8 | Partial | 1 | Feb 17, 2026 |
intro h
have hp_p : Nat.Prime (p : ℕ) := hp
have h_p_gt_one : 1 < (p : ℕ) := Nat.Prime.one_lt hp_p
have h_p_dvd : (p : ℕ) ∣ classNumber (maximalRealSubfield (CyclotomicField p ℚ)) := h
|
View{
"agent_telemetry": {
"compilations": 1,
"iterations": 1,
"duration_s": 106.49,
"best_status": "partial",
"best_goals": 1,
"max_iterations": 8,
"model": "gemini-3-flash-preview",
"error": "Gemini API error 429: {\n \"error\": {\n \"code\": 429,\n \"message\": \"Resource has been exhausted (e.g. check quota).\",\n \"status\": \"RESOURCE_EXHAUSTED\"\n }\n}\n",
"provider": "gemini_direct",
"finish_reason": "STOP",
"usage": {
"prompt_tokens": 1753,
"completion_tokens": 100,
"total_tokens": 17045,
"reasoning_tokens": 15192,
"cost_usd": 0.0
},
"reasoning_effort": "",
"response_trace_count": 2
},
"response_trace": [
{
"iteration": 1,
"provider": "gemini_direct",
"finish_reason": "STOP",
"api_elapsed_s": 83.895,
"usage": {
"prompt_tokens": 1753,
"completion_tokens": 100,
"total_tokens": 17045,
"reasoning_tokens": 15192,
"cost_usd": 0.0
},
"thoughts_tokens": 15192,
"gemini_retries": 0,
"has_function_call": true,
"response_text_len": 0,
"model_text_preview": ""
},
{
"iteration": 1,
"event": "compile_proof",
"provider": "gemini_direct",
"status": "partial",
"goals_remaining": 1,
"timed_out": false,
"banned_tokens": [],
"proof_code": "intro h\nhave hp_p : Nat.Prime (p : \u2115) := hp\nhave h_p_gt_one : 1 < (p : \u2115) := Nat.Prime.one_lt hp_p\nhave h_p_dvd : (p : \u2115) \u2223 classNumber (maximalRealSubfield (CyclotomicField p \u211a)) := h",
"compiler_output_preview": "[path]:17:72: error: unsolved goals\np : \u2115+\nhp : p.Prime\nh : \u2191p \u2223 classNumber \u21a5(maximalRealSubfield (CyclotomicField \u2191p \u211a))\nhp_p : Nat.Prime \u2191p\nh_p_gt_one : 1 < \u2191p\nh_p_dvd : \u2191p \u2223 classNumber \u21a5(maximalRealSubfield (CyclotomicField \u2191p \u211a))\n\u22a2 False\n'kummer_vandiver' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]\n\n"
}
],
"verification": {
"banned_tokens": [],
"command": [
"[path]
"lean",
"[path]
],
"duration_s": 7.910107612609863,
"goals_remaining": 1,
"is_verified": false,
"lean_file_path": "[path]
"problem": {
"axioms_check_name": "kummer_vandiver",
"axioms_check_skipped": false,
"benchmark_id": "Wikipedia__KummerVandiver__kummer_vandiver",
"category": "research_open",
"endings": [],
"imports": [
"FormalConjectures.Util.ProblemImports"
],
"preamble_chars": 183,
"source_file": "FormalConjectures/Wikipedia/KummerVandiver.lean",
"title": "kummer_vandiver"
},
"returncode": 1,
"status": "partial",
"stderr": "",
"stdout": "[path]:17:72: error: unsolved goals\np : \u2115+\nhp : p.Prime\nh : \u2191p \u2223 classNumber \u21a5(maximalRealSubfield (CyclotomicField \u2191p \u211a))\nhp_p : Nat.Prime \u2191p\nh_p_gt_one : 1 < \u2191p\nh_p_dvd : \u2191p \u2223 classNumber \u21a5(maximalRealSubfield (CyclotomicField \u2191p \u211a))\n\u22a2 False\n'kummer_vandiver' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]\n",
"timed_out": false
}
}
|
| Gemini 3 Flash Preview | Failed | -- | Feb 14, 2026 |
unfold classNumber
set K := CyclotomicField p ℚ
set L := maximalRealSubfield K
by_contra h
let h_div := h
clear h
induction p using PNat.recOn
case h p =>
simp at hp
have : p.Prime := hp
aesop
|
View{
"generation": {
"attempts": 1,
"banned_tokens_found": [],
"elapsed_s": 3.46,
"finish_reason": "stop",
"max_tokens": 8192,
"model_id": "google/gemini-3-flash-preview",
"proof_code_length": 198,
"raw_content_length": 1073,
"reasoning_effort": "",
"structured_output": true,
"temperature": 0.0,
"usage": {
"completion_tokens": 273,
"completion_tokens_details": {
"image_tokens": 0,
"reasoning_tokens": 0
},
"cost": 0.001607,
"cost_details": {
"upstream_inference_completions_cost": 0.000819,
"upstream_inference_cost": 0.001607,
"upstream_inference_prompt_cost": 0.000788
},
"is_byok": false,
"prompt_tokens": 1576,
"prompt_tokens_details": {
"audio_tokens": 0,
"cache_write_tokens": 0,
"cached_tokens": 0,
"video_tokens": 0
},
"total_tokens": 1849
}
},
"verification": {
"banned_tokens": [],
"command": [
"[path]
"lean",
"[path]
],
"duration_s": 7.348396301269531,
"goals_remaining": null,
"is_verified": false,
"lean_file_path": "[path]
"problem": {
"benchmark_id": "Wikipedia__KummerVandiver__kummer_vandiver",
"category": "research_open",
"endings": [],
"imports": [
"FormalConjectures.Util.ProblemImports"
],
"preamble_chars": 183,
"source_file": "FormalConjectures/Wikipedia/KummerVandiver.lean",
"title": "kummer_vandiver"
},
"returncode": 1,
"status": "failed",
"stderr": "",
"stdout": "[path]:23:2: error: tactic 'clear' failed, variable 'h_div' depends on 'h'\np : \u2115+\nhp : p.Prime\nK : Type := CyclotomicField \u2191p \u211a\nL : Subfield K := maximalRealSubfield K\nh : \u2191p \u2223 Fintype.card (ClassGroup (\ud835\udcde \u21a5L))\nh_div : \u2191p \u2223 Fintype.card (ClassGroup (\ud835\udcde \u21a5L)) := h\n\u22a2 False\n",
"timed_out": false
}
}
|