Back to Problems
pi_pow_exp_transcendental
Specification
$\pi^e$ is transcendental.
Lean 4 Statement
theorem pi_pow_exp_transcendental : Transcendental ℚ (π ^ (exp 1))
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": 39.61,
"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": 24851,
"completion_tokens": 1629,
"total_tokens": 26480,
"reasoning_tokens": 1378,
"cost_usd": 0.03645845
},
"reasoning_effort": "high",
"response_trace_count": 10
},
"response_trace": [
{
"iteration": 1,
"event": "search_mathlib",
"query": "transcendental_pi",
"results_count": 0
},
{
"iteration": 2,
"event": "search_mathlib",
"query": "Transcendental \u211a \u03c0",
"results_count": 0
},
{
"iteration": 3,
"event": "search_mathlib",
"query": "pi",
"results_count": 1
},
{
"iteration": 4,
"event": "search_mathlib",
"query": "Transcendental",
"results_count": 1
},
{
"iteration": 5,
"event": "search_mathlib",
"query": "Real.transcendental",
"results_count": 8
},
{
"iteration": 6,
"event": "search_mathlib",
"query": "pi_pow_exp_transcendental",
"results_count": 8
},
{
"iteration": 7,
"event": "search_mathlib",
"query": "transcendental_exp",
"results_count": 0
},
{
"iteration": 8,
"event": "search_mathlib",
"query": "Real.transcendental_exp",
"results_count": 8
},
{
"iteration": 9,
"event": "search_mathlib",
"query": "pow_e_transcendental",
"results_count": 1
},
{
"iteration": 10,
"event": "search_mathlib",
"query": "Transcendental.pow",
"results_count": 1
}
]
}
|
|
| Gemini 3.1 Pro Agent v8 | Failed | -- | Feb 24, 2026 |
View{
"agent_telemetry": {
"compilations": 0,
"iterations": 0,
"duration_s": 0.04,
"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 |
unfold Transcendental
intro h
let α := π ^ (exp 1)
have h_α : IsAlgebraic ℚ α := h
let e := exp 1
have h_pi_e : α = π ^ e := rfl
have h_trans_pi : Transcendental ℚ π := transcendental_pi
have h_trans_e : Transcendental ℚ e := transcendental_e
let log_α := Log α
have h_log : log_α = e * Log π := ?_
cases' h_α with p hp
induction p using Polynomial.induction_on
· simp at hp
· skip
· skip
apply h_trans_pi
exact ?_
|
View{
"agent_telemetry": {
"compilations": 8,
"iterations": 8,
"duration_s": 104.15,
"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": 35217,
"completion_tokens": 1408,
"total_tokens": 36625,
"reasoning_tokens": null,
"cost_usd": 0.01273935
},
"reasoning_effort": "",
"response_trace_count": 16
},
"response_trace": [
{
"iteration": 1,
"provider": "openrouter_primary",
"finish_reason": "stop",
"response_id": "gen-1771350422-HiKt8dj8nqiTjbYUg01k",
"api_elapsed_s": 13.453,
"usage": {
"prompt_tokens": 1573,
"completion_tokens": 154,
"total_tokens": 1727,
"reasoning_tokens": null,
"cost_usd": 0.0012485
},
"openrouter_retries": 0,
"response_text_len": 414
},
{
"iteration": 1,
"event": "compile_proof",
"provider": "openrouter_primary",
"status": "failed",
"goals_remaining": null,
"timed_out": false,
"banned_tokens": [],
"proof_code": "unfold Transcendental\nintro h\nlet \u03b1 := \u03c0 ^ (exp 1)\nhave h_\u03b1 : IsAlgebraic \u211a \u03b1 := h\nlet e := exp 1\nhave h_pi_e : \u03b1 = \u03c0 ^ e := rfl\nhave h_trans_pi : Transcendental \u211a \u03c0 := transcendental_pi\nhave h_trans_e : Transcendental \u211a e := transcendental_e\nlet log_\u03b1 := Log \u03b1\nhave h_log : log_\u03b1 = e * Log \u03c0 := ?_\ncases' h_\u03b1 with p hp\ninduction p using Polynomial.induction_on\n\u00b7 simp at hp\n\u00b7 skip\n\u00b7 skip\napply h_trans_pi\nexact ?_",
"compiler_output_preview": "[path]:25:42: error: unknown identifier 'transcendental_pi'\n[path]:26:41: error: unknown identifier 'transcendental_e'\n[path]
},
{
"iteration": 2,
"provider": "openrouter_primary",
"finish_reason": "stop",
"response_id": "gen-1771350444-5A7bInei4EJZMysVQndF",
"api_elapsed_s": 14.261,
"usage": {
"prompt_tokens": 2395,
"completion_tokens": 128,
"total_tokens": 2523,
"reasoning_tokens": null,
"cost_usd": 0.0015815
},
"openrouter_retries": 0,
"response_text_len": 328
},
{
"iteration": 2,
"event": "compile_proof",
"provider": "openrouter_primary",
"status": "failed",
"goals_remaining": null,
"timed_out": false,
"banned_tokens": [],
"proof_code": "unfold Transcendental\nintro h\nlet \u03b1 := \u03c0 ^ (rexp 1)\nhave h_\u03b1 : IsAlgebraic \u211a \u03b1 := h\nlet e := rexp 1\nhave h_pi : Transcendental \u211a \u03c0 := by\n exact transcendental_pi\nhave h_e : Transcendental \u211a e := by\n exact transcendental_e\nlet L := log \u03b1\nhave h_log : L = e * log \u03c0 := by\n simp [\u03b1, e]\n exact log_rpow pi_pos (rexp 1)\nrefine ?_",
"compiler_output_preview": "[path]:25:10: error: unknown identifier 'transcendental_pi'\n[path]:27:10: error: unknown identifier 'transcendental_e'\n[path]
},
{
"iteration": 3,
"provider": "openrouter_primary",
"finish_reason": "stop",
"response_id": "gen-1771350466-EpaQ4R7kRMJyvKeK7Lf6",
"api_elapsed_s": 1.785,
"usage": {
"prompt_tokens": 3144,
"completion_tokens": 163,
"total_tokens": 3307,
"reasoning_tokens": null,
"cost_usd": 0.00115425
},
"openrouter_retries": 0,
"response_text_len": 389
},
{
"iteration": 3,
"event": "compile_proof",
"provider": "openrouter_primary",
"status": "failed",
"goals_remaining": null,
"timed_out": false,
"banned_tokens": [],
"proof_code": "unfold Transcendental\nintro h\nlet \u03b1 := \u03c0 ^ (rexp 1)\nhave h_\u03b1 : IsAlgebraic \u211a \u03b1 := h\nlet e := rexp 1\nhave h_trans_pi : Transcendental \u211a \u03c0 := by\n exact Real.transcendental_pi\nhave h_trans_e : Transcendental \u211a e := by\n exact Real.transcendental_e\nlet l_\u03b1 := log \u03b1\nhave h_log : l_\u03b1 = e * log \u03c0 := by\n dsimp [l_\u03b1, \u03b1, e]\n rw [log_rpow pi_pos]\nobtain \u27e8p, hp_nonzero, hp_root\u27e9 := h_\u03b1\nrefine ?_",
"compiler_output_preview": "[path]:25:10: error: unknown constant 'Real.transcendental_pi'\n[path]:27:10: error: unknown constant 'Real.transcendental_e'\n[path]
},
{
"iteration": 4,
"provider": "openrouter_primary",
"finish_reason": "stop",
"response_id": "gen-1771350475-ks7ysw1f67ajdm0SDoXR",
"api_elapsed_s": 2.218,
"usage": {
"prompt_tokens": 3860,
"completion_tokens": 198,
"total_tokens": 4058,
"reasoning_tokens": null,
"cost_usd": 0.00161635
},
"openrouter_retries": 0,
"response_text_len": 455
},
{
"iteration": 4,
"event": "compile_proof",
"provider": "openrouter_primary",
"status": "failed",
"goals_remaining": null,
"timed_out": false,
"banned_tokens": [],
"proof_code": "unfold Transcendental\nintro h\nlet \u03b1 := \u03c0 ^ (rexp 1)\nobtain \u27e8p, hp_nz, hp_root\u27e9 := h\nhave h_pi_pos : 0 < \u03c0 := pi_pos\nhave h_e : rexp 1 = exp 1 := rfl\nhave h_\u03b1_def : \u03b1 = \u03c0 ^ exp 1 := rfl\nlet log_\u03b1 := log \u03b1\nhave h_log_\u03b1 : log_\u03b1 = exp 1 * log \u03c0 := by\n rw [h_\u03b1_def, log_rpow h_pi_pos (exp 1)]\nlet \u03b2 := exp 1\nhave h_\u03b2_trans : Transcendental \u211a \u03b2 := by\n exact exp_one_transcendental\nhave h_pi_trans : Transcendental \u211a \u03c0 := by\n exact pi_transcendental\nrefine ?_",
"compiler_output_preview": "[path]:28:8: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression\n \u03b1\n\u03b1 : \u211d := \u03c0 ^ rexp 1\np : Polynomial \u211a\nhp_nz : p \u2260 0\nhp_root : (Polynomial.aeval (\u03c0 ^ rexp 1)) p = 0\nh_pi_pos : 0 < \u03c0\nh_e : rexp 1 = rexp 1\nh_\u03b1_def : \u03b1 = \u03c0 ^ rexp 1\nlog_\u03b1 : \u211d := log \u03b1\n\u22a2 log_\u03b1 = rexp 1 * log \u03c0\n[path]
},
{
"iteration": 5,
"provider": "openrouter_primary",
"finish_reason": "stop",
"response_id": "gen-1771350485-WqtGvbqpteJedG3QDudo",
"api_elapsed_s": 2.165,
"usage": {
"prompt_tokens": 4846,
"completion_tokens": 179,
"total_tokens": 5025,
"reasoning_tokens": null,
"cost_usd": 0.002051
},
"openrouter_retries": 0,
"response_text_len": 412
},
{
"iteration": 5,
"event": "compile_proof",
"provider": "openrouter_primary",
"status": "failed",
"goals_remaining": null,
"timed_out": false,
"banned_tokens": [],
"proof_code": "intro h\nobtain \u27e8p, hp_nz, hp_root\u27e9 := h\nhave h_pi_pos : 0 < \u03c0 := Real.pi_pos\nhave h_trans_pi : Transcendental \u211a \u03c0 := Real.pi_transcendental\nhave h_trans_e : Transcendental \u211a (rexp 1) := Real.exp_one_transcendental\nlet \u03b1 := \u03c0 ^ (rexp 1)\nhave h_log_\u03b1 : Real.log \u03b1 = (rexp 1) * Real.log \u03c0 := by\n dsimp [\u03b1]\n rw [Real.log_rpow h_pi_pos]\nlet i := Complex.I\nlet log_\u03b1_c : \u2102 := Complex.log (Complex.ofReal \u03b1)\nrefine ?_",
"compiler_output_preview": "[path]:22:42: error: unknown constant 'Real.pi_transcendental'\n[path]:23:48: error: unknown constant 'Real.exp_one_transcendental'\n[path]
},
{
"iteration": 6,
"provider": "openrouter_primary",
"finish_reason": "stop",
"response_id": "gen-1771350495-AMREoWIZaweHgPtdb7aE",
"api_elapsed_s": 1.923,
"usage": {
"prompt_tokens": 5684,
"completion_tokens": 135,
"total_tokens": 5819,
"reasoning_tokens": null,
"cost_usd": 0.00142765
},
"openrouter_retries": 0,
"response_text_len": 335
},
{
"iteration": 6,
"event": "compile_proof",
"provider": "openrouter_primary",
"status": "failed",
"goals_remaining": null,
"timed_out": false,
"banned_tokens": [],
"proof_code": "unfold Transcendental\nintro h\nlet \u03b1 := \u03c0 ^ rexp 1\nhave h_\u03b1 : IsAlgebraic \u211a \u03b1 := h\nobtain \u27e8p, hp_nz, hp_root\u27e9 := h_\u03b1\nlet e := rexp 1\nset log_\u03c0 := Real.log \u03c0\nhave h1 : Transcendental \u211a \u03c0 := by\n exact Real.pi_transcendental\nhave h2 : Transcendental \u211a e := by\n exact Real.exp_one_transcendental\nlet f : \u2102 := \u03c0 ^ (Complex.I : \u2102)\nrefine ?_",
"compiler_output_preview": "[path]:27:10: error: unknown constant 'Real.pi_transcendental'\n[path]:29:10: error: unknown constant 'Real.exp_one_transcendental'\n[path]
},
{
"iteration": 7,
"provider": "openrouter_primary",
"finish_reason": "stop",
"response_id": "gen-1771350505-9A6RevVlm2ZTQVBnGQL3",
"api_elapsed_s": 2.539,
"usage": {
"prompt_tokens": 6455,
"completion_tokens": 252,
"total_tokens": 6707,
"reasoning_tokens": null,
"cost_usd": 0.0021637
},
"openrouter_retries": 0,
"response_text_len": 547
},
{
"iteration": 7,
"event": "compile_proof",
"provider": "openrouter_primary",
"status": "failed",
"goals_remaining": null,
"timed_out": false,
"banned_tokens": [],
"proof_code": "unfold Transcendental\nintro h\nlet \u03b1 := \u03c0 ^ (rexp 1)\nhave h_\u03b1 : IsAlgebraic \u211a \u03b1 := h\nlet e := rexp 1\nlet log_pi := Real.log \u03c0\nhave h_pi_pos : 0 < \u03c0 := Real.pi_pos\nhave h_log_\u03b1 : Real.log \u03b1 = e * log_pi := by\n dsimp [\u03b1, e, log_pi]\n rw [Real.log_rpow h_pi_pos]\n\nlet \u03b1_c : \u2102 := Complex.ofReal \u03b1\nlet e_c : \u2102 := Complex.ofReal e\nlet pi_c : \u2102 := Complex.ofReal \u03c0\n\nhave h_pi_c_nz : pi_c \u2260 0 := by\n simp [pi_c]\n exact Real.pi_ne_zero\n\nhave h_\u03b1_c_alg : IsAlgebraic \u211a \u03b1_c := by\n exact IsAlgebraic.of_real h_\u03b1\n\nobtain \u27e8p, hp_nz, hp_root\u27e9 := h_\u03b1\nrefine ?_",
"compiler_output_preview": "[path]:36:4: error: no goals to be solved\n[path]:39:10: error: unknown constant 'IsAlgebraic.of_real'\n[path]:18:70: error: un\n...<truncated>"
},
{
"iteration": 8,
"provider": "openrouter_primary",
"finish_reason": "stop",
"response_id": "gen-1771350516-GF3ElXLp0peSDIUYW3ln",
"api_elapsed_s": 2.396,
"usage": {
"prompt_tokens": 7260,
"completion_tokens": 199,
"total_tokens": 7459,
"reasoning_tokens": null,
"cost_usd": 0.0014964
},
"openrouter_retries": 0,
"response_text_len": 400
},
{
"iteration": 8,
"event": "compile_proof",
"provider": "openrouter_primary",
"status": "failed",
"goals_remaining": null,
"timed_out": false,
"banned_tokens": [],
"proof_code": "unfold Transcendental\nintro h\nlet \u03b1 := \u03c0 ^ rexp 1\nobtain \u27e8p, hp_nz, hp_root\u27e9 := h\nhave h_pi_pos : 0 < \u03c0 := Real.pi_pos\nhave h_log_\u03b1 : Real.log \u03b1 = (rexp 1) * Real.log \u03c0 := by\n dsimp [\u03b1]\n rw [Real.log_rpow h_pi_pos]\nlet \u03b1_c : \u2102 := (\u03b1 : \u2102)\nlet pi_c : \u2102 := (\u03c0 : \u2102)\nlet e_c : \u2102 := (rexp 1 : \u2102)\nhave h_alg_\u03b1 : IsAlgebraic \u211a \u03b1_c := by\n use p, hp_nz\n rw [Complex.aeval_ofReal]\n simp [hp_root]\nrefine ?_",
"compiler_output_preview": "[path]:32:8: error: unknown constant 'Complex.aeval_ofReal'\n[path]:18:70: error: unsolved goals\ncase intro.intro\n\u03b1 : \u211d := \u03c0 ^ rexp 1\np : Polynomial \u211a\nhp_nz : p \u2260 0\nhp_root : (Polynomial.aeval (\u03c0 ^ rexp 1)) p = 0\nh_pi_pos : 0 < \u03c0\nh_log_\u03b1 : log \u03b1 = rex\n...<truncated>"
}
],
"verification": {
"banned_tokens": [],
"command": [
"[path]
"lean",
"[path]
],
"duration_s": 7.480010747909546,
"goals_remaining": null,
"is_verified": false,
"lean_file_path": "[path]
"problem": {
"axioms_check_name": "pi_pow_exp_transcendental",
"axioms_check_skipped": false,
"benchmark_id": "Wikipedia__Transcendental__pi_pow_exp_transcendental",
"category": "research_open",
"endings": [
"end Transcendental"
],
"imports": [
"FormalConjectures.Util.ProblemImports"
],
"preamble_chars": 167,
"source_file": "FormalConjectures/Wikipedia/Transcendental.lean",
"title": "pi_pow_exp_transcendental"
},
"returncode": 1,
"status": "failed",
"stderr": "",
"stdout": "[path]:25:42: error: unknown identifier 'transcendental_pi'\n[path]:26:41: error: unknown identifier 'transcendental_e'\n[path]:27:15: error: unknown identifier 'Log'\n[path]:18:70: error: unsolved goals\nh : IsAlgebraic \u211a (\u03c0 ^ rexp 1)\n\u03b1 : \u211d := \u03c0 ^ rexp 1\nh_\u03b1 : IsAlgebraic \u211a \u03b1\ne : \u211d := rexp 1\nh_pi_e : \u03b1 = \u03c0 ^ e\nh_trans_pi : Transcendental \u211a \u03c0\nh_trans_e : Transcendental \u211a e\n\u22a2 False\n'Transcendental.pi_pow_exp_transcendental' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]\n",
"timed_out": false
}
}
|
| Gemini 3 Flash Preview | Failed | -- | Feb 14, 2026 |
rw [log_rpow pi_pos]
ring
have h_exp : exp (e * log π) = x := by
rw [exp_log pi_pos]
rfl
exact (transcendental_pi h_is_alg)
|
View{
"generation": {
"attempts": 1,
"banned_tokens_found": [],
"elapsed_s": 3.87,
"finish_reason": "stop",
"max_tokens": 8192,
"model_id": "google/gemini-3-flash-preview",
"proof_code_length": 129,
"raw_content_length": 1105,
"reasoning_effort": "",
"structured_output": true,
"temperature": 0.0,
"usage": {
"completion_tokens": 333,
"completion_tokens_details": {
"image_tokens": 0,
"reasoning_tokens": 0
},
"cost": 0.0017695,
"cost_details": {
"upstream_inference_completions_cost": 0.000999,
"upstream_inference_cost": 0.0017695,
"upstream_inference_prompt_cost": 0.0007705
},
"is_byok": false,
"prompt_tokens": 1541,
"prompt_tokens_details": {
"audio_tokens": 0,
"cache_write_tokens": 0,
"cached_tokens": 0,
"video_tokens": 0
},
"total_tokens": 1874
}
},
"verification": {
"banned_tokens": [],
"command": [
"[path]
"lean",
"[path]
],
"duration_s": 7.725633382797241,
"goals_remaining": null,
"is_verified": false,
"lean_file_path": "[path]
"problem": {
"benchmark_id": "Wikipedia__Transcendental__pi_pow_exp_transcendental",
"category": "research_open",
"endings": [
"end Transcendental"
],
"imports": [
"FormalConjectures.Util.ProblemImports"
],
"preamble_chars": 167,
"source_file": "FormalConjectures/Wikipedia/Transcendental.lean",
"title": "pi_pow_exp_transcendental"
},
"returncode": 1,
"status": "failed",
"stderr": "",
"stdout": "[path]:19:6: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression\n log (\u03c0 ^ ?y)\n\u22a2 Transcendental \u211a (\u03c0 ^ rexp 1)\n[path]:20:4: error: unexpected identifier; expected command\n",
"timed_out": false
}
}
|