Cyrup

Problem Statement

Cyrup is a decentralized marketplace that connects people who need mathematical proofs with expert theorem provers. The platform bridges the gap between theoretical computer science and practical verification needs by creating an economic incentive layer for formal verification.At its core, Cyrup allows users to post mathematical or logical challenges that require formal proofs, set USDC rewards, and have experts submit solutions using the Lean 4 theorem prover. The platform features a sophisticated reputation system that tracks user performance and ensures only qualified verifiers (top 10% by reputation) can validate submissions.The system operates through smart contracts deployed on Base Sepolia, ensuring transparent and automatic reward distribution. When a proof is submitted, it goes through both automated verification via a Lean 4 runner service and human verification by qualified experts. Once both the challenge creator and assigned verifier approve a solution, rewards are automatically distributed - 95% to the solver and 5% to the verifier.Key features include an integrated web-based Lean IDE for writing proofs directly in the browser, a comprehensive leaderboard system, gas-optimized smart contracts using clone patterns and packed storage, and a persistent Lean verification service that validates proofs in real-time.

Solution

Smart Contracts (Solidity/Foundry):Built with ultra-optimized Solidity contracts using packed structs, custom errors, and the clone pattern for gas efficiencyChallengeFactory deploys minimal proxy clones using CREATE2 for deterministic addressesChallengeEscrow manages the lifecycle: challenge creation → verifier selection → solution submission → dual approval → automatic reward distributionReputationSystem implements dynamic top 10% tracking with efficient threshold algorithms and tiered point calculation based on USDC amountsDeployed on Base Sepolia for low-cost transactionsBackend (Go/Gin):Microservices architecture with two separate services: API server and Lean runnerAPI server built with Gin framework handles HTTP requests, database operations (PostgreSQL via sqlx), and queues verification requestsLean runner service runs in a Docker container with persistent Lean 4 environment, avoiding restart overhead between verificationsServices communicate via HTTP, deployable on Railway with automatic port detection and internal networkingImplements submission tracking with unique UIDs linking blockchain transactions to off-chain Lean codeFrontend (Next.js/React):Next.js 14 app with TypeScript, Tailwind CSS for styling, and wagmi/viem for Web3 integrationCoinbase CDP SDK integration for streamlined wallet connections and transaction signingMonaco Editor integration provides a full-featured IDE for writing Lean proofs in the browserReact Markdown with syntax highlighting for rendering challenge descriptionsCustom hooks abstract contract interactions and API callsLean 4 Integration:Docker containerized Lean 4 environment with pre-built mathlib for fast verificationHTTP service wrapper around Lean that accepts code, verifies proofs, and returns resultsPersistent container architecture eliminates cold start delaysDatabase stores proof code with IPFS hashes for permanent storageNotable Technical Achievements:Gas optimization through clone pattern saves ~90% deployment costs per challengePacked storage reduces state variables from 8+ slots to 3-4 slots per structBitmap approval system tracks dual signatures in single uint8Dynamic reputation threshold algorithm efficiently maintains top 10% without full sortingMicroservices architecture allows independent scaling of verification workloadIntegration of formal verification (Lean 4) with blockchain creates trustless proof marketplace