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:
  4a54eb04b7bcd0c3f9b1a00df6512b09020631ad8539b61c8d869e678be4cd62
proof, sha256 (8 lines, 451 bytes):
  fd5c334cadb0d774f89605bee3c9f7842ee8072242aa80e4bdc99ff1c071e2c3

[1/4] word filter .... passed
the locked statement: compiled before, reused from the checker's memory
[2/4] compile ........ 4 errors (4.00 s)
  proof line 2, column 66: Application type mismatch: The argument
      hp3
    has type
      3 < p
    but is expected to have type
      2 < p
    in the application
      ne_of_gt hp3
  proof line 3, column 26: Invalid field `mod_three_ne_zero_of_ne_three`: The environment does not contain `Irreducible.mod_three_ne_zero_of_ne_three`, so it is not possible to project the field `mod_three_ne_zero_of_ne_three` from an expression
      hp
    of type `Irreducible p`
  proof line 4, column 28: Application type mismatch: The argument
      Nat.prime_three
    has type
      Nat.Prime 3
    but is expected to have type
      ?m.77 ≠ 1
    in the application
      Nat.Prime.dvd_iff_eq hp Nat.prime_three
  at the theorem: unsolved goals
    p : ℕ
    hp : Nat.Prime p
    hp3 : 3 < p
    h1 : p % 2 = 1
    h2 : p % 3 ≠ 0
    ⊢ 24 ∣ p ^ 2 - 1

VERDICT: REFUSED (compile)
Lean refused the proof at line 2: Application type mismatch: The argument

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.