Lean 4 proofs, checked by the kernel, of the things mathematicians never bothered to prove: that a market maker can't be drained, that a quorum survives its faults, that a secret stays secret.
Mathlib is the community's library of mathematics. This is a library of everything else that happens to be provable.
A market maker no trade sequence can arbitrage. A consensus protocol that holds as long as fewer than a third of its
nodes lie. An auction where honesty is the best strategy. A secret split into shares, where any t of them rebuild
it and any t−1 tell you nothing. Each result lives in one .lean file that opens with import Mathlib, and the
Lean kernel checks it alone: #print axioms shows the three standard axioms and nothing else, and no file hides a
sorry.
A system called LeanMill wrote every proof here, starting from a blueprint in plain English. LeanMill renders the blueprint into a Lean statement, runs that statement past a firewall to confirm it still says what the blueprint said, searches for a proof, and re-checks the closed proof against a governance kernel the proving agent has no way to reach. The human writes the blueprint; the apparatus writes the Lean.
Formal verification was, until a year ago, the most labour-starved corner of software. Fluency in Lean or Coq belongs to mathematicians and cryptographers, with every reason to formalize perfectoid spaces and none to formalize a credit-agreement covenant. Fluency in the covenant, the payment waterfall, the quorum rule, and the pricing bound belongs to a different population, one that never learned to write a proof. Between the two sat the messy, high-value logic that runs money and institutions, left unverified because a specialist at $300k a year spending six months on a single covenant never paid for itself.
An engine that formalizes on its own drops that cost to the price of the compute it burns. nonmathlib4 collects
what falls out. And the results build on each other: a later proof cites an earlier banked one instead of proving it
again, so the library is the ground the engine stands on, and it grows.
| Domain | Results |
|---|---|
Finance/ |
Constant-product AMM temporal + no-arbitrage invariants; no round-trip arbitrage at any reachable pool state; corporate absolute-priority and pari-passu waterfalls; fundamental theorem of asset pricing (both directions: easy, and the hard Stiemke/separation direction — no arbitrage ⇒ strictly positive state prices) |
Strategy/ |
Topkis supermodular and ordinal/single-crossing monotone comparative statics; VCG dominant-strategy incentive-compatibility with pivot independence and a two-unit witness |
DistributedSystems/ |
Byzantine quorum intersection: safe + available threshold quorums exist iff n ≥ 3f + 1 |
Cryptography/ |
Shamir (t, n) threshold secret sharing: reconstruction from any t shares, perfect-secrecy bijection from any t − 1, boundary tightness |
Compliance/ |
A real high-yield restricted-payments covenant (SEC EDGAR): the engine abstracts the accounting from a natural-language directive, proves the covenant's safety invariants, and a faithfulness certificate refutes each laundered reading with a concrete distinguishing transaction |
SocialChoice/ |
Black's median voter theorem; Gale-Shapley deferred acceptance: complete strict preferences and quiescence imply stability, while a non-quiescent reachable state can still contain a blocking pair |
Probability/ |
Bayesian screening: the positive predictive value of a test clears one-half exactly when the true-positive mass meets the false-positive mass, and for any imperfect specificity there is a low enough prevalence where even a perfectly sensitive test's positive result is more likely wrong than right — the base-rate fallacy, mechanized |
Governance/ |
Corporate charter adoption as a two-gate conjunction (quorum and a present-basis supermajority), with the basis load-bearing: a tally can clear the supermajority on votes cast yet fail it on shares present, the divergence driven by a strictly positive abstention |
blueprints/ |
The natural-language inputs — one per theorem family, the only human-authored artifact |
Each domain folder carries its own README, a per-theorem summary, and a scope caveat wherever the formalization proves a core rather than the full security or economic statement. Shamir is the honest example: it proves the algebraic secrecy bijection, not the measure-theoretic Shannon statement.
lake exe cache get # fetch the Mathlib build cache (v4.30.0-rc2)
lake build # kernel-check every filed theorem
Toolchain: leanprover/lean4:v4.30.0-rc2, Mathlib pinned to the same tag.
Consume it like any Lake dependency. In your lakefile.toml:
[[require]]
name = "nonmathlib4"
git = "https://github.com/sparckix/nonmathlib4"
rev = "main"Then import whichever result you want:
import Nonmathlib.Finance.ConstantProductAmm -- one resultSibling files define their own vocabulary and share top-level names on purpose (both AMM files define Trade, for
instance), so the kernel checks each one on its own rather than folding them into a single environment. lake build
compiles and kernel-checks all of them. Your project has to sit on leanprover/lean4:v4.30.0-rc2 with Mathlib pinned
to that tag; one Lean version resolves Lean, Mathlib, and this library together.
Or take a file, not a dependency. Every module here stands alone. It opens with import Mathlib, defines its own
vocabulary, and cites nothing from a sibling, so you can drop one .lean into any Mathlib project and it elaborates
as written, no require needed. Mathlib's own files work the opposite way, too interdependent to lift out one at a
time. The blueprint that produced each theorem sits beside it in blueprints/, and a provenance
header records how it was built.
Read a theorem here the way a skeptic would, and four things back it up.
The proofs are autoformalized, not hand-written. Your blueprint is the human input; the apparatus writes the Lean
statement, clears it through the faithfulness firewall, and finds the proof. Every filed theorem is a closure the
kernel ratified on its own, carrying a matched-negative-control receipt and a passing governance kernel that audits
for laundering, statement drift, and stray axioms. #print axioms comes back propext, Classical.choice,
Quot.sound, with no sorryAx.
The one thing the kernel does not certify is meaning. It confirms the proof follows from the stated definitions; it cannot confirm those definitions say what you think they say. So wherever a theorem proves a core rather than the full real-world property, the folder README tells you, in plain language, exactly where the guarantee stops.
MIT. See LICENSE.