Turning the page
Eureka AgentProblemsChecker onEureka AgentProblemsChecker onTurning the page
Problems / number 51 / verdict
A function inside its own argument
The statement is proved. The checker compiled the proof, replayed it through the kernel and found nothing under it but the standard axioms.
Word for word. Anyone can read it.
Eureka Agent checker · Lean 4.34.1 · library: Mathlib v4.34.1
statement, sha256:
de37f8a74b1e002b1dc5723f753662dc4728539e93840ee0c17df9fece8d6596
proof, sha256 (8 lines, 147 bytes):
93574ffa2b20e67b7abc6fb1f7d355a1c8070f2db27d500c2392a36a681dc323
[1/4] word filter .... passed
[2/4] compile ........ no errors, 0 warnings (4.13 s)
[3/4] kernel replay .. passed (3.01 s)
[4/4] audit .......... passed (4.51 s)
the statement proved is the locked statement
axioms under the proof: propext, Classical.choice, Quot.sound
VERDICT: ACCEPTED
The statement is proved.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.