# Lean proofs for the Polymarket fee research 24 October 2026 · Lean 4.35.0 · Exact-rational arithmetic · No Mathlib dependency This package checks the fee mathematics and selected published figures in [How Polymarket Makes Money: $46.6 Million in Taker Fees in Four Months](https://vultax.com/research/how-does-polymarket-make-money). The machine-readable result is `verification.json`. The package contains the frozen public research exports, formal statements and proofs, axiom audit, a verifier, failure controls, and a CI workflow. Source snapshots are dated and SHA-256 hashed in `sources.json`. The compressed exported proof terms and their dependencies are included as `evidence/proof-dependencies.ndjson.gz`; the hash of the decompressed export is recorded in the verifier result. ## What is checked `FeeResearch.lean` contains 13 general research theorems and one arithmetic helper. It proves, for the defined exact-rational model: - The fee is nonnegative for nonnegative shares and rate, with price between zero and one. - The dollar fee is symmetric around a 50¢ price and reaches a maximum there for fixed nonnegative shares and rate. - A zero rate produces zero fee. The unrounded fee is additive in share quantity at the same price and rate; this theorem makes no assertion about separately rounded fills. - For positive shares and price, fee divided by stake equals `rate × (1 − price)`. At a nonnegative rate, that fraction cannot increase as price rises. - Break-even equals `price × (1 + rate × (1 − price))`. - With positive shares, expected profit is nonnegative exactly when win probability meets or exceeds that break-even threshold. - The threshold is no lower than price under the fee-domain assumptions, and no higher than one when the rate is at most one and price lies between zero and one. `PublishedChecks.lean` contains 12 concrete calculation theorems. They check: - All **57 values** in the published fee-percentage chart, across 19 prices and three reference rates. - The sports and crypto worked examples, the favourite's break-even threshold, the maximum probability increments, and the stated longshot fee percentages. - Arithmetic and headline-rounding consistency of **17 displayed aggregate estimates**: ten month rows and seven category rows. Both totals support the rounded $46.6M headline. The displayed monthly total is $46,639,686 and the category total is $46,639,685, a $1 difference. The proof establishes that difference and the rounding intervals; it does not establish the cause of the difference or reconcile unrounded raw fills. - The published April, crypto and sports rounded amounts, the 67.1% crypto share, the under-$1M remainder, and the zero values for the six displayed 2025 months. The last check does not extend the chart's coverage to undisplayed months. The 26 theorem declarations include one helper. The count is an inventory, not a percentage of the article or system verified. ## Model and trust boundary Shares pay $1 on a win and zero on a loss. Prices and fee rates are fractions, and monetary amounts are dollars. The expected-profit model charges one entry fee and excludes rebates, spreads, later sale costs, time value and unavailable fills. All proofs use rational arithmetic, rather than IEEE floating point or an exchange's rounding implementation. The dated reference rates are 0.07, 0.05 and 0.04 as stated in the study's 25 September 2026 schedule. Whether those rates applied to a particular historical or current market is an external input, not a theorem in this package. The checks **do not formally verify** the acquisition or completeness of the 714,691,643 historical fills, the classification of each fill's fee schedule, the underlying $46.6M reconstruction, actual collected fees or maker payouts, current rates, production JavaScript/Python, or the feasibility/profitability of a trade. The historical headline's arithmetic is checked against the displayed exports; the underlying empirical measurement remains separate. Theorems are checked by Lean, audited for transitive axiom dependencies, replayed through Lean's kernel, and exported with their dependencies to the external Nanoda Rust checker. Only Lean's standard `propext`, `Classical.choice` and `Quot.sound` axioms are permitted. Proof placeholders, custom axioms and native-evaluation assumptions are rejected. These are automated checks, with the formal statements and scope reviewed during implementation. No independent human review or certification is claimed. The bundled Nanoda checker can report an “Unable to print axioms” pretty-printer diagnostic while confirming no type-checker errors; the verifier records it. Pretty-printer output is not used as proof evidence. ## Reproduce With Lean 4.35.0 already available: ```sh python3 scripts/verify.py ``` Or point to its binaries: ```sh python3 scripts/bootstrap_verify.py --lean-bin /absolute/path/to/lean-4.35.0-linux/bin ``` On Linux x86_64, this command downloads and checks the official release archive in a project-local cache, without changing shell configuration or a global Lean installation: ```sh python3 scripts/bootstrap_verify.py ``` The pinned archive's URL, length and SHA-256 are in `toolchain-release.json`. The archive is about 594 MB compressed and requires additional extraction space. Python 3.11+ and `tar`/`zstd` are required for the bootstrap route. Other platforms can install the pinned Lean version and use `scripts/verify.py`. The verifier checks frozen-source hashes and deterministic generation, builds the project, audits every theorem, runs kernel replay and Nanoda, and confirms that an altered chart cell, an injected false axiom and a proof placeholder are rejected. `--skip-independent-checker` is available for troubleshooting and produces an explicitly reduced verification status. The GitHub workflow runs this same command when this directory is used as a repository root. It is supplied as source; no remote CI run is claimed. No ongoing monitor or new scheduled job was created. ## Updating the study Keep source snapshots and recorded URLs together. A new source edition requires a new capture and hash record, review of the statements and reference rates, regeneration with `python3 scripts/generate_checks.py`, and a full verifier run. Do not replace a failed proof with an axiom or a placeholder. A changed empirical estimate can require a changed concrete theorem; the new statement needs review rather than silently inheriting the old verification claim. The proof source and frozen exports can be attached to the study as a versioned package. Website publication must follow the existing release process and capacity controls. This source package does not itself change the public article. ## Attribution and references The source article is Vultax Research, published by OmniOS OÜ. It credits Boka Qin and Rui Yang's [Polymarket-v1 dataset](https://huggingface.co/datasets/TimeSeventeen/Polymarket-v1), CC BY 4.0, for its historical fills. The raw fill dataset is not included in this package. Source and data credits in the frozen article and JSON are preserved. The proof project was generated and checked with Codex; AI assistance is not an independent endorsement. The official Lean distribution is used as tooling and is not bundled in the source ZIP. - [Lean proof-validation guidance](https://lean-lang.org/doc/reference/latest/ValidatingProofs/) - [Lean axiom guidance](https://lean-lang.org/doc/reference/latest/Axioms/) - [Nanoda external checker](https://github.com/ammkrn/nanoda_lib) - [Polymarket's fee formula](https://docs.polymarket.com/trading/fees)