Sponsor

Keep the corpus free.

Nasrudin's verified-theorem corpus is built by volunteer worker compute and stays free forever. Sponsorships fund what volunteers can't carry: central Lean4 re-verification, API hosting, the embedding index, and the engineering time to keep all of it running.

Sponsorship is a donation, not a subscription tier — you don't get extra targeted searches or higher API quotas. You get the satisfaction of knowing this stays open. If you want service-tier access to commission targeted compute, see Pricing.

Coffee

$5 / month

Buys ~one hour of Lean4 verification time. Keeps the lights on and the workers fed.

Pizza

$25 / month

Underwrites a slice of the central re-verification cluster. The corpus stays open because of you.

Cluster Hour

$100 / month

Sponsors meaningful targeted-search compute and lets us point cycles at open conjectures with no paying buyer attached.

Prefer a one-time gift?

Name your amount →

Hosted by Stripe · choose any amount from $5

Where the money goes

Operating costs, in order.

Central Lean4 re-verification — every worker submission is independently re-checked on our side before joining the global corpus.
Embedding index hosting — semantic search over the whole corpus runs on hardware that costs money to keep online.
API and frontend — Postgres, RocksDB, the web UI, KaTeX rendering.
Engineering time — keeping the GA, the prover bridge, and the ingest pipeline alive and improving.