Accepted

Log of the check

Word for word. Anyone can read it.

Eureka Agent checker · Lean 4.34.1 · library: core
statement, sha256:
  eda7497b7cd6d98535851e429ea64c6badaacf9c7c7988ac6035b1a36b8c03e0
proof, sha256 (20 lines, 406 bytes):
  d4f58271b066fc499c0e9ed9d6fd7a9d1b4e35ad363f1179cd8c7f9ab706b692

[1/4] word filter .... passed
[2/4] compile ........ no errors, 0 warnings (0.38 s)
[3/4] kernel replay .. passed (3.34 s)
[4/4] audit .......... passed (0.27 s)
      the statement proved is the locked statement
      axioms under the proof: propext

VERDICT: ACCEPTED
The statement is proved.

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.