Back to Problems
rlog_pi_transcendental
Specification
$\log(\pi)$ is transcendental.
Lean 4 Statement
theorem rlog_pi_transcendental : Transcendental ℚ (log π)
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": 4,
"duration_s": 308.81,
"best_status": "pending",
"best_goals": null,
"max_iterations": 10,
"model": "openai/gpt-5.3-codex",
"error": "OpenRouter API total timeout after 330s (model=openai/gpt-5.3-codex) [non_retryable]",
"provider": "openrouter_primary",
"finish_reason": "tool_calls",
"usage": {
"prompt_tokens": 6907,
"completion_tokens": 379,
"total_tokens": 7286,
"reasoning_tokens": 273,
"cost_usd": 0.00932925
},
"reasoning_effort": "high",
"response_trace_count": 4
},
"response_trace": [
{
"iteration": 1,
"event": "search_mathlib",
"query": "transcendental_log_pi",
"results_count": 5
},
{
"iteration": 2,
"event": "search_mathlib",
"query": "Transcendental \u211a (log \u03c0)",
"results_count": 0
},
{
"iteration": 3,
"event": "search_mathlib",
"query": "transcendental_pi",
"results_count": 0
},
{
"iteration": 4,
"event": "search_mathlib",
"query": "Transcendental \u03c0",
"results_count": 0
}
]
}
|
|
| Gemini 3.1 Pro Agent v8 | Failed | -- | Feb 24, 2026 |
View{
"agent_telemetry": {
"compilations": 0,
"iterations": 0,
"duration_s": 0.07,
"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 | Failed | -- | Feb 17, 2026 |
intro h
have h_pos : 0 < π := pi_pos
have h_ne_one : π ≠ 1 := by
refine ne_of_gt ?_
exact pi_gt_one
have h_exp : exp (log π) = π := exp_log h_pos
have h_trans : Transcendental ℚ π := by
exact pi_transcendental
by_contra h_alg
have h_log_alg : IsAlgebraic ℚ (log π) := by
exact h_alg
obtain ⟨f, f_poly, f_root⟩ := h_log_alg
have h_pi_alg : IsAlgebraic ℚ π := by
rw [← h_exp]
exact IsAlgebraic.exp_of_isAlgebraic h_log_alg
exact h_trans h_pi_alg
|
View{
"agent_telemetry": {
"compilations": 8,
"iterations": 8,
"duration_s": 94.49,
"best_status": "failed",
"best_goals": null,
"max_iterations": 8,
"model": "gemini-3-flash-preview",
"error": null,
"provider": "openrouter_primary",
"finish_reason": "stop",
"usage": {
"prompt_tokens": 31188,
"completion_tokens": 1005,
"total_tokens": 32193,
"reasoning_tokens": null,
"cost_usd": 0.0122577
},
"reasoning_effort": "",
"response_trace_count": 16
},
"response_trace": [
{
"iteration": 1,
"provider": "openrouter_primary",
"finish_reason": "stop",
"response_id": "gen-1771350609-z1qSYhjv9jjFIbrwJL7f",
"api_elapsed_s": 14.201,
"usage": {
"prompt_tokens": 1566,
"completion_tokens": 196,
"total_tokens": 1762,
"reasoning_tokens": null,
"cost_usd": 0.001371
},
"openrouter_retries": 1,
"response_text_len": 455
},
{
"iteration": 1,
"event": "compile_proof",
"provider": "openrouter_primary",
"status": "failed",
"goals_remaining": null,
"timed_out": false,
"banned_tokens": [],
"proof_code": "intro h\nhave h_pos : 0 < \u03c0 := pi_pos\nhave h_ne_one : \u03c0 \u2260 1 := by\n refine ne_of_gt ?_\n exact pi_gt_one\nhave h_exp : exp (log \u03c0) = \u03c0 := exp_log h_pos\nhave h_trans : Transcendental \u211a \u03c0 := by\n exact pi_transcendental\nby_contra h_alg\nhave h_log_alg : IsAlgebraic \u211a (log \u03c0) := by\n exact h_alg\nobtain \u27e8f, f_poly, f_root\u27e9 := h_log_alg\nhave h_pi_alg : IsAlgebraic \u211a \u03c0 := by\n rw [\u2190 h_exp]\n exact IsAlgebraic.exp_of_isAlgebraic h_log_alg\nexact h_trans h_pi_alg",
"compiler_output_preview": "[path]:23:10: error: unknown identifier 'pi_gt_one'\n[path]:26:10: error: unknown identifier 'pi_transcendental'\n[path]:29:4: error: ty\n...<truncated>"
},
{
"iteration": 2,
"provider": "openrouter_primary",
"finish_reason": "stop",
"response_id": "gen-1771350623-sdncxJrEzQPqwzYctNf7",
"api_elapsed_s": 1.789,
"usage": {
"prompt_tokens": 2419,
"completion_tokens": 148,
"total_tokens": 2567,
"reasoning_tokens": null,
"cost_usd": 0.0016535
},
"openrouter_retries": 0,
"response_text_len": 389
},
{
"iteration": 2,
"event": "compile_proof",
"provider": "openrouter_primary",
"status": "failed",
"goals_remaining": null,
"timed_out": false,
"banned_tokens": [],
"proof_code": "intro h_alg\nhave h_pos : 0 < \u03c0 := pi_pos\nhave h_exp : exp (log \u03c0) = exp_log h_pos\nhave h_pi_alg : IsAlgebraic \u211a \u03c0 := by\n have : IsAlgebraic \u211a (exp (log \u03c0)) := by\n apply Transcendental.LindemannWeierstrass.isAlgebraic_exp_of_isAlgebraic\n exact h_alg\n rw [h_exp] at this\n exact this\nhave h_pi_trans : Transcendental \u211a \u03c0 := by\n apply Real.pi_transcendental\nexact h_pi_trans h_pi_alg",
"compiler_output_preview": "[path]:21:29: error: type mismatch\n exp_log h_pos\nhas type\n rexp (log \u03c0) = \u03c0 : Prop\nbut is expected to have type\n \u211d : Type\n[path]:24:12: error: unknown constant 'Transcendental.LindemannWeierstrass.isAlgebraic_exp_of_isAlgebraic'\n[path]
},
{
"iteration": 3,
"provider": "openrouter_primary",
"finish_reason": "stop",
"response_id": "gen-1771350633-uspuJT9B8Afw589AVzSk",
"api_elapsed_s": 1.462,
"usage": {
"prompt_tokens": 3381,
"completion_tokens": 90,
"total_tokens": 3471,
"reasoning_tokens": null,
"cost_usd": 0.0019605
},
"openrouter_retries": 0,
"response_text_len": 223
},
{
"iteration": 3,
"event": "compile_proof",
"provider": "openrouter_primary",
"status": "failed",
"goals_remaining": null,
"timed_out": false,
"banned_tokens": [],
"proof_code": "intro h_log_alg\nhave h_pos : 0 < \u03c0 := pi_pos\nhave h_pi_alg : IsAlgebraic \u211a \u03c0 := by\n rw [\u2190 exp_log h_pos]\n exact IsAlgebraic.exp h_log_alg\nhave h_pi_trans : Transcendental \u211a \u03c0 := transcendental_pi\nexact h_pi_trans h_pi_alg",
"compiler_output_preview": "[path]:23:10: error: unknown constant 'IsAlgebraic.exp'\n[path]:24:42: error: unknown identifier 'transcendental_pi'\n'Transcendental.rlog_pi_transcendental' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]\n\n"
},
{
"iteration": 4,
"provider": "openrouter_primary",
"finish_reason": "stop",
"response_id": "gen-1771350642-JyG2uDufJ5fHjDBdNgf3",
"api_elapsed_s": 8.257,
"usage": {
"prompt_tokens": 3759,
"completion_tokens": 98,
"total_tokens": 3857,
"reasoning_tokens": null,
"cost_usd": 0.0012663
},
"openrouter_retries": 0,
"response_text_len": 238
},
{
"iteration": 4,
"event": "compile_proof",
"provider": "openrouter_primary",
"status": "failed",
"goals_remaining": null,
"timed_out": false,
"banned_tokens": [],
"proof_code": "intro h_log_alg\nhave h_pos : 0 < \u03c0 := Real.pi_pos\nhave h_pi_alg : IsAlgebraic \u211a \u03c0 := by\n rw [\u2190 Real.exp_log h_pos]\n exact IsAlgebraic.exp h_log_alg\nhave h_pi_trans : Transcendental \u211a \u03c0 := Real.transcendental_pi\nexact h_pi_trans h_pi_alg",
"compiler_output_preview": "[path]:23:10: error: unknown constant 'IsAlgebraic.exp'\n[path]:24:42: error: unknown constant 'Real.transcendental_pi'\n'Transcendental.rlog_pi_transcendental' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]\n\n"
},
{
"iteration": 5,
"provider": "openrouter_primary",
"finish_reason": "stop",
"response_id": "gen-1771350658-A8c9qRmtlJ7IYXwyqiH2",
"api_elapsed_s": 1.667,
"usage": {
"prompt_tokens": 4219,
"completion_tokens": 131,
"total_tokens": 4350,
"reasoning_tokens": null,
"cost_usd": 0.0025025
},
"openrouter_retries": 0,
"response_text_len": 365
},
{
"iteration": 5,
"event": "compile_proof",
"provider": "openrouter_primary",
"status": "failed",
"goals_remaining": null,
"timed_out": false,
"banned_tokens": [],
"proof_code": "intro h_log_alg\nhave h_pos : 0 < \u03c0 := pi_pos\nhave h_pi_alg : IsAlgebraic \u211a \u03c0 := by\n rw [\u2190 exp_log h_pos]\n -- Use Lindemann-Weierstrass for exp\n exact Transcendental.isAlgebraic_exp_of_isAlgebraic h_log_alg\nhave h_pi_trans : Transcendental \u211a \u03c0 := by\n -- Pi is transcendental is a known constant in Mathlib\n exact Real.transcendental_pi\nexact h_pi_trans h_pi_alg",
"compiler_output_preview": "[path]:24:10: error: unknown constant 'Transcendental.isAlgebraic_exp_of_isAlgebraic'\n[path]:27:10: error: unknown constant 'Real.transcendental_pi'\n'Transcendental.rlog_pi_transcendental' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]\n...<truncated>"
},
{
"iteration": 6,
"provider": "openrouter_primary",
"finish_reason": "stop",
"response_id": "gen-1771350668-5xyepL8VMekeX9ZNxFot",
"api_elapsed_s": 1.537,
"usage": {
"prompt_tokens": 4805,
"completion_tokens": 107,
"total_tokens": 4912,
"reasoning_tokens": null,
"cost_usd": 0.00090865
},
"openrouter_retries": 0,
"response_text_len": 261
},
{
"iteration": 6,
"event": "compile_proof",
"provider": "openrouter_primary",
"status": "failed",
"goals_remaining": null,
"timed_out": false,
"banned_tokens": [],
"proof_code": "intro h_log_alg\nhave h_pos : 0 < \u03c0 := pi_pos\nhave h_exp : exp (log \u03c0) = \u03c0 := exp_log h_pos\nhave h_pi_alg : IsAlgebraic \u211a \u03c0 := by\n rw [\u2190 h_exp]\n exact IsAlgebraic.exp h_log_alg\nhave h_pi_trans : Transcendental \u211a \u03c0 := transcendental_pi\nexact h_pi_trans h_pi_alg",
"compiler_output_preview": "[path]:24:10: error: unknown constant 'IsAlgebraic.exp'\n[path]:25:42: error: unknown identifier 'transcendental_pi'\n'Transcendental.rlog_pi_transcendental' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]\n\n"
},
{
"iteration": 7,
"provider": "openrouter_primary",
"finish_reason": "stop",
"response_id": "gen-1771350677-0RUt9J8A2MBzA2Ps9pIE",
"api_elapsed_s": 1.864,
"usage": {
"prompt_tokens": 5200,
"completion_tokens": 120,
"total_tokens": 5320,
"reasoning_tokens": null,
"cost_usd": 0.0011456
},
"openrouter_retries": 0,
"response_text_len": 299
},
{
"iteration": 7,
"event": "compile_proof",
"provider": "openrouter_primary",
"status": "failed",
"goals_remaining": null,
"timed_out": false,
"banned_tokens": [],
"proof_code": "intro h_log_alg\nhave h_pos : 0 < \u03c0 := pi_pos\nhave h_pi_alg : IsAlgebraic \u211a \u03c0 := by\n have h_exp := exp_log h_pos\n rw [\u2190 h_exp]\n apply Transcendental.isAlgebraic_exp_of_isAlgebraic\n exact h_log_alg\nhave h_pi_trans : Transcendental \u211a \u03c0 := by\n exact Real.transcendental_pi\nexact h_pi_trans h_pi_alg",
"compiler_output_preview": "[path]:24:10: error: unknown constant 'Transcendental.isAlgebraic_exp_of_isAlgebraic'\n[path]:25:4: error: no goals to be solved\n[path]
},
{
"iteration": 8,
"provider": "openrouter_primary",
"finish_reason": "stop",
"response_id": "gen-1771350686-PUnYfDHFBy8mNGZP27nw",
"api_elapsed_s": 1.717,
"usage": {
"prompt_tokens": 5839,
"completion_tokens": 115,
"total_tokens": 5954,
"reasoning_tokens": null,
"cost_usd": 0.00144965
},
"openrouter_retries": 0,
"response_text_len": 259
},
{
"iteration": 8,
"event": "compile_proof",
"provider": "openrouter_primary",
"status": "failed",
"goals_remaining": null,
"timed_out": false,
"banned_tokens": [],
"proof_code": "intro h_log_alg\nintro h_pi_alg\nhave h_pos : 0 < \u03c0 := pi_pos\nhave h_exp_log : exp (log \u03c0) = \u03c0 := exp_log h_pos\nhave h_trans_pi : Transcendental \u211a \u03c0 := by\n refine ?_\nhave h_alg_pi : IsAlgebraic \u211a \u03c0 := by\n rw [\u2190 h_exp_log]\n refine ?_\nexact h_trans_pi h_alg_pi",
"compiler_output_preview": "[path]:20:8: error: tactic 'introN' failed, insufficient number of binders\nh_log_alg : IsAlgebraic \u211a (log \u03c0)\n\u22a2 False\n'Transcendental.rlog_pi_transcendental' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]\n\n"
}
],
"verification": {
"banned_tokens": [],
"command": [
"[path]
"lean",
"[path]
],
"duration_s": 8.134364604949951,
"goals_remaining": null,
"is_verified": false,
"lean_file_path": "[path]
"problem": {
"axioms_check_name": "rlog_pi_transcendental",
"axioms_check_skipped": false,
"benchmark_id": "Wikipedia__Transcendental__rlog_pi_transcendental",
"category": "research_open",
"endings": [
"end Transcendental"
],
"imports": [
"FormalConjectures.Util.ProblemImports"
],
"preamble_chars": 167,
"source_file": "FormalConjectures/Wikipedia/Transcendental.lean",
"title": "rlog_pi_transcendental"
},
"returncode": 1,
"status": "failed",
"stderr": "",
"stdout": "[path]:23:10: error: unknown identifier 'pi_gt_one'\n[path]:26:10: error: unknown identifier 'pi_transcendental'\n[path]:29:4: error: type mismatch\n h_alg\nhas type\n \u00acFalse : Prop\nbut is expected to have type\n IsAlgebraic \u211a (log \u03c0) : Prop\n[path]:33:10: error: unknown constant 'IsAlgebraic.exp_of_isAlgebraic'\n'Transcendental.rlog_pi_transcendental' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]\n",
"timed_out": false
}
}
|
| Gemini 3 Flash Preview | Failed | -- | Feb 14, 2026 |
apply Algebraic.exp
exact h
rw [exp_log (by positivity)] at h_exp
have h_pi : Transcendental ℚ π := transcendental_pi
exact h_pi h_exp
|
View{
"generation": {
"attempts": 1,
"banned_tokens_found": [],
"elapsed_s": 3.9,
"finish_reason": "stop",
"max_tokens": 8192,
"model_id": "google/gemini-3-flash-preview",
"proof_code_length": 136,
"raw_content_length": 859,
"reasoning_effort": "",
"structured_output": true,
"temperature": 0.0,
"usage": {
"completion_tokens": 241,
"completion_tokens_details": {
"image_tokens": 0,
"reasoning_tokens": 0
},
"cost": 0.001491,
"cost_details": {
"upstream_inference_completions_cost": 0.000723,
"upstream_inference_cost": 0.001491,
"upstream_inference_prompt_cost": 0.000768
},
"is_byok": false,
"prompt_tokens": 1536,
"prompt_tokens_details": {
"audio_tokens": 0,
"cache_write_tokens": 0,
"cached_tokens": 0,
"video_tokens": 0
},
"total_tokens": 1777
}
},
"verification": {
"banned_tokens": [],
"command": [
"[path]
"lean",
"[path]
],
"duration_s": 7.494422674179077,
"goals_remaining": null,
"is_verified": false,
"lean_file_path": "[path]
"problem": {
"benchmark_id": "Wikipedia__Transcendental__rlog_pi_transcendental",
"category": "research_open",
"endings": [
"end Transcendental"
],
"imports": [
"FormalConjectures.Util.ProblemImports"
],
"preamble_chars": 167,
"source_file": "FormalConjectures/Wikipedia/Transcendental.lean",
"title": "rlog_pi_transcendental"
},
"returncode": 1,
"status": "failed",
"stderr": "",
"stdout": "[path]:19:8: error: unknown identifier 'Algebraic.exp'\n[path]:21:6: error: no goals to be solved\n",
"timed_out": false
}
}
|