The corpus is open by principle — built by volunteer compute and free forever. What we charge for is targeted compute: the slices of GA cluster you point at your own conjecture, plus the API that lets you build on top of Nasrudin.
Yes. Every verified theorem is browseable, downloadable as a .lean file, and re-verifiable on your own machine without a paid plan. The corpus is built by volunteer worker compute and stays free by design.
You provide a conjecture in Lean syntax (or natural language we transcribe). We dedicate a slice of the GA cluster to evolve toward it for up to 24 hours. Paid tiers buy targeted compute aimed at *your* conjecture — the open corpus is never gated.
Yes. Self-serve cancel from the billing portal — your plan stays active through the end of the current period.
No cash. Workers earn (1) attribution on every theorem they verify, (2) leaderboard rank, and (3) — coming soon — a free Researcher tier when contributing ≥10 hours of verification time per month. Compute donated by workers builds the open corpus; paid tiers buy targeted GA slices pointed at the buyer's own conjecture.
No — Nasrudin is for anyone pointing compute at hard problems. Independent researchers, industry R&D, quant teams, and academics with budget all use it the same way. Verified academic email gets 50% off Researcher.