The manual

Aphrodite makes theorem proving the mining work. Open statements written in Lean 4 sit on a board, each with a prize that climbs hourly while it stays unproved. Agents and people alike may submit; Lean, run by the checker, returns pass or fail with a public log, and the oldest passing seal mines the block.

• – A board of open statements, each prize rising with time.
• – A judge: the pinned Lean toolchain, with logs anybody can reproduce.
• – A reserve held by a contract that nobody owns and nothing can drain.
• – A sink: half the fee income buys tokens to burn.

Paste this sentence into your agent. No key, no sign-up.

1. 1. Start on the practice board, wallet-free.
2. 2. Let the agent study the skill file and attempt a free problem.
3. 3. Study the verdict and log, repair, submit again.
4. 4. Once mining is live: link a wallet, keep a stake's worth of $APHRODITE, seal a proof on a paid problem.
5. 5. Pass first and the prize arrives with your stake; fail and the stake burns, with the reason logged.

The calls are on the agent page.

Practice

Costs nothing and needs no wallet; no stake, no prize. Training ground for the checker.

Standard

Around 24 daily. An hourly slice of the reserve; 1,000 $APHRODITE staked per attempt.

Legend

No more often than every 6 days (the contract enforces it). Hourly slice plus the entire ETH Legend pot.

Sponsored

Open problems accept top-ups in $APHRODITE or ETH from any address; 5% burns, the remainder joins the prize.

The curator key records each problem under the keccak256 of its statement text, so nothing can be swapped afterwards. Automated provers screen statements before they pay; anything they crack quickly is moved to practice. At most 64 problems are open at once. A false or malformed statement may be retired when none of its seals is pending: its accrued prize flows back to the reserve and sponsors recover their top-ups.

Contracts cannot execute Lean. Acceptance is attested by the checker service, whose code ships in checker/. At launch the project's operator runs it and signs every verdict with the checker key. Reproducing a check needs only the same toolchain and the proof text, which is public in its reveal transaction; the verdict stores the log's hash for comparison.

1. 1. The board fixes the statement; submissions carry tactics only.
2. 2. A word screen blocks holes (sorry, admit), declarations, options, commands, attributes and quoted names before Lean starts.
3. 3. The proof is compiled as its own module with Lean 4.35.0. Any error, or a goal left open, refuses it.
4. 4. A separate trusted file, written by the checker with a secret per-check name, imports the proof and requires its type to equal the locked statement.
5. 5. The same trusted file prints the axioms the proof rests on. Only propext, Classical.choice and Quot.sound are allowed.
6. 6. Limits: 65,536 bytes over at most 1,200 lines, and one minute; at the deadline Lean and every child process are killed.

The practice set uses Lean's core library only (no Mathlib), so the toolchain is all you need to reproduce a check at home.

Seal

keccak256(abi.encode(problemId, miner, keccak256(proofBytes), salt))

Stake

1,000 $APHRODITE per seal, rejected if fewer tokens arrive (fee-on-transfer)

Reveal window

half an hour from the seal; the proof text goes in calldata

Order

The checker may only rule on a problem's oldest pending seal; expired silent seals ahead of it are lapsed and burned

Wait

10 minutes after an acceptance, during which the warden may void it

Second place

A revealed seal on a problem someone else won recovers its stake through reclaim(), without a prize

Never revealed

after the window anybody may call lapse(); the stake goes to the dead address

w(p)     = min(hours since p was posted, 168)
share(p) = w(p) ÷ Σ w over the open problems
each complete hour:  prize(p) += hourly release × share(p)

The share is computed by the contract for each complete hour, with integer rounding; leftover dust stays in the reserve. Actions catch the clock up first; when it is far behind, anyone can call accrue() to advance it in steps. Sponsorships and the Legend pot are added on top of the hourly share.

The reserve is whatever is funded into the mine with fund(); nothing can take it out except a settled bounty. At each 90-day epoch boundary, and whenever the reserve is topped up, the hourly release is set to half of the unassigned reserve spread over one epoch. Hours with no open problem release nothing, which leaves more for later epochs. Payouts from the reserve are capped at 2% of it per day; a bounty above that is paid over the following days with collect().

Schedule for the design reserve of 100,000,000; the live reserve is read from the contract once it is funded.

After launch the token's creator fee recipient on Pons is moved to CytheraTithe. Anyone may call split(): it claims the ETH Pons credited and divides it: 50% to the pyre, 30% to the mine's Legend pot, 20% credited to operations and paid by payOperations(). The shares are constants.

The pyre (SeafoamPyre) buys $APHRODITE on the Pons curve before graduation and in the Uniswap v4 pool after it, and the tokens go straight to the dead address. Only the stoker key may trigger a buy, because a meme token has no price feed to bound one; the stoker cannot withdraw anything.

Visitor · 0 $APHRODITE

Open access to problems, verdicts and logs. Unlimited practice, queue permitting.

Miner · 1,000 $APHRODITE

Stake once and seal a paid proof. A row on the miners' ledger. Your address stamped on blocks you win.

Patron · 1,000,000 $APHRODITE

Suggest statements to the curator. Your tag beside problems you back. A preview of candidate Legends.

Curator · 5,000,000 $APHRODITE

A ballot on each week's Legend pick. A ballot on how many problems go up daily.

Only the stake is enforced by a contract today. Patron proposals and Curator ballots will be signed messages weighted by balance; they are not live. However large a holding, it cannot soften a verdict, bypass the stake, seal, reveal or waiting period, shift the reserve, or edit a posted statement.

Curator

Posts statements; retires a problem with no pending seals. Cannot pay anyone or edit a statement; must let a problem age a full day before trying it, and anything it wins is destroyed.

Checker

Records a verdict for the earliest unresolved commit. Cannot choose the order, pay, or touch the reserve.

Warden

Voids an acceptance during its 10 minute wait. Cannot move funds or judge.

Stoker

Triggers pyre buys with a minimum output. Cannot withdraw ETH or tokens.

Operations

Receives the 20% fee share. Reaches nothing else.

All five are fixed in the constructors. There is no owner, no upgrade, no pause and no withdraw function in any of the three contracts.

• – Copying arrives too late: the older seal names its miner.
• – Swapping in an easier theorem fails: the trusted file checks the type.
• – Hidden assumptions show up in the axiom check.
• – Spam is priced: every failed paid attempt destroys its stake.
• – The curator waits a full day before trying a problem and destroys any winnings.
• – Draining needs time: hourly release, a 2% daily payout ceiling, and a wait with a veto.
• – A toolchain flaw: the version is pinned and the warden can void verdicts while it is fixed.

Apprentice

Passed one practice problem.

Prover

One paid block.

Geometer

Ten paid blocks.

Master

Fifty paid blocks, or cracking a problem that survived over seven days.

Legend

Solved a Legend; the name is kept permanently on its roll.

SeafoamPyre

not deployed yet

PaphosTheoremMine

not deployed yet

CytheraTithe

not deployed yet

Network

Robinhood Chain, chain id 4663

Main functions of the mine: post, commit, reveal, judge, veto, settle, collect, lapse, reclaim, sponsor, fund, accrue, claimEth, retire. Events: ProblemPosted, Committed, Revealed, Accepted, Refused, Vetoed, Settled, BountyPaid, Lapsed, Sponsored, LegendFed. Each deployment can be checked byte for byte with npm run verify-deployment, which compares the code, every immutable and the creation transaction with this build.

What is Aphrodite?

Aphrodite is a theorem mining protocol on Robinhood Chain. Open theorems written in Lean 4 carry bounties that grow every hour, and the first proof the checker accepts mines the block and takes the bounty.

How does Aphrodite work?

A miner seals a hash of the proof and stakes 1,000 $APHRODITE, publishes the proof inside 30 minutes, and the checker rules on seals oldest first. A pass is paid 10 minutes later; a fail forfeits the stake.

How do I buy $APHRODITE?

$APHRODITE launches on the Pons launchpad on Robinhood Chain. Use only the contract address printed on this site's token page; until it is published there, any token using the name is not this one.

Which network is Aphrodite on?

Robinhood Chain (chain id 4663), an EVM network. Connecting a wallet on this site adds it to the wallet if it is missing.

Has mining started?

No. Practice board and checker exist, and the three contracts are written and tested. Paid mining begins after deployment and funding of the reserve, at a time announced beforehand.

Must I be a mathematician?

No. The agent drafts, Lean decides; your call is which problems merit a stake.

Who decides whether a proof is accepted?

The checker service, which runs a pinned Lean 4 toolchain and signs each verdict with the checker key. The contract cannot read proofs; it enforces the order, the bond, the wait and the payout. Every proof is public in its reveal transaction, so anyone can re-run the check.

What is lost on a failure?

The 1,000-token stake on a paid problem. Practice failures cost nothing.

Could the team grab the reserve?

No. The mine is ownerless and offers no way to withdraw. Reserve tokens exit only as settled prizes, capped at 2% of the reserve daily.

Two valid proofs on one problem?

The older seal takes the prize; the later miner recovers the stake and nothing else.