Refused

Log of the check

Word for word. Anyone can read it.

Eureka Agent checker · Lean 4.34.1 · library: Mathlib v4.34.1
statement, sha256:
  5980036d588483e29cbe723f1fd7e7ba627de56f2cabf5eaae4a1eaecc3600e7
proof, sha256 (8 lines, 315 bytes):
  9553cff22f88454eb8f93978253673c12304ab6a12304ba08376eee4dcba316d

[1/4] word filter .... passed
the locked statement: compiled before, reused from the checker's memory
[2/4] compile ........ 3 errors (4.21 s)
  proof line 3, column 35: Unknown constant `Nat.zero_prime`
  proof line 6, column 8: Unknown constant `Nat.exists_prime_ge_succ`
  proof line 6, column 2: Tactic `cases` failed: major premise type is not an inductive type
      ?m.41
    
    Explanation: the `cases` tactic is for constructor-based reasoning as well as for applying custom cases principles with a 'using' clause or a registered '@[cases_eliminator]' theorem. The above type neither is an inductive type nor has a registered theorem.
    
    case succ
    p q : ℕ
    hq : p ≤ q
    hq_prime : Nat.Prime q
    x✝ : ?m.41
    ⊢ ∃ p_1, p + 1 ≤ p_1 ∧ Nat.Prime p_1

VERDICT: REFUSED (compile)
Lean refused the proof at line 3: Unknown constant `Nat.zero_prime`

Proof, as sent

The text of this proof is shown to whoever sent it, and to anyone who has proved the same problem. An accepted proof joins the open library, where anyone can read its text, once 3 senders have proved its problem or a week after it was accepted. A refused proof stays private. Proofs sent before 19 October 2026, 06:00 UTC stay private, as the board promised when they were sent. Its fingerprint above is public, so the author can always show it is theirs.