Development

Getting the code

The source is not public. There is no repository URL to publish yet, and no licence file in the tree — so nothing on this site is currently something you can clone, build or audit independently. Access is by request.

That is a real limitation on every claim made here, and it is stated first rather than last: a proof you cannot run is a claim about a proof. The commands below describe how the development is built by someone who has the tree.

The trusted computing base

For a reviewer this is the number that matters, and it is unusually small.

Component	What it is
Lean toolchain	`leanprover/lean4:v4.28.0`, pinned in `lean-toolchain`
External Lean dependencies	None. The lakefile declares no `require` at all — no Mathlib, nothing
Axioms	Standard only: `propext`, `Classical.choice`, `Quot.sound`. Many headline results depend on none
Solidity	solc 0.8.28, Hardhat 3; no external libraries; three contracts + one library

No Mathlib is the load-bearing fact. The entire development is built on Lean core, so a reviewer's trust base is the Lean kernel and nothing else — no community library, no unaudited dependency graph, no version skew. It also explains why the proofs are written the way they are: arithmetic is Nat, and finite claims are discharged by decide rather than by library lemmas.

Install the toolchain with elan:

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
elan toolchain install leanprover/lean4:v4.28.0

Layout

DoreFormal/        the Lean 4 development — 81 targets, no sorry, no axioms
dore-contracts/    Hardhat project — 4 contracts, 19 tests
docs-site/         this documentation
encyclopedia/      the product corpus and the legal source registry

The formal development

lake build          # 81 targets
.claude/bin/loop-test   # build + hygiene gate

The hygiene gate fails on any sorry, admit, native_decide, custom axiom or compiler warning. Axiom audits are run on every headline theorem; the development uses only propext, Classical.choice and Quot.sound, and many results use none.

The contracts

cd dore-contracts
yarn install
npx hardhat test

Tests are named after the theorems they discharge. If a contract changes such that a named property no longer holds, the test that fails tells you which proof you have contradicted.

The documentation

cd docs-site
npm install
npm run dev        # local
npm run build      # static output in dist/

House rules

Never claim a theorem that does not exist. A docstring in this project once named a theorem as the thing binding two halves of a module together; the theorem did not exist, and the halves were unconnected. Grep every name you cite before shipping.

Report frontiers, not tuned successes. Where a result depends on an unverified input, publish the boundary at which it changes rather than picking an input that makes it pass.

Say what is not modeled. Each module carries an explicit "is not grounded" section. Those sections are the most useful part of the development to a reader deciding how much weight to put on it.