Lean Research
Notebook

LEAN × VERSO · EXPERIMENT 001

A checked design.
An open question.

What happens when an experiment challenges its own assumptions?

Follow a small research loop from a formally checked design to synthetic evidence and a better next question.

Synthetic evidence only

THE RESEARCH LOOP

Explore the experiment

Committed example · a96aa5e
Lean-checked design

Four treatments.
Two nuisance factors.

A 4 × 4 Latin square assigns each treatment exactly once in every row and column. The first round uses shift 0, giving four observations per treatment.

Rows and columns stand for fixed nuisance conditions. Balance is a mathematical property; it does not prove that a treatment works.

16initial observations
6advertised theorems
Inspect the Lean declarations ↗

The certified family

SHIFT 0
RowC0C1C2C3
0

All four shifts are checked in Lean. Shifts 1–3 become the follow-up in this example.

treatment = (row + column + shift) mod 4
Browser visualization of committed source and reportNo live Lean execution or model inference

A DIFFERENT STANDARD FOR EACH CLAIM

What is actually known?

The notebook keeps proof, computation, observation, and judgment separate. Select a category to inspect its boundary.

UNDER THE NOTEBOOK

A small, inspectable chain

  1. 01 / AUTHOR

    Verso Manual

    Lean-native document with checked code cells and recorded proof-state hovers.

  2. 02 / CHECK

    Lean kernel

    Balance, counts, complete coverage, and an exact integer additive identity.

  3. 03 / OBSERVE

    Python harness

    A seeded generator, blocked analysis, and a bounded data-only proposal.

  4. 04 / RECORD

    Provenance

    Hashed sources and artifacts, recomputed analysis, and rejection of stale inputs.

Proof fields are erased during execution. Exported JSON is data, not a portable proof certificate. Hashes check consistency; they are not signatures.

READ IT. RUN IT. CHANGE IT.

The source is the notebook.

Lean 4.34.0 and Verso are pinned. The local harness uses Python 3.11+ and its standard library. No model, API key, GPU, or Python packages are required.

You’ll need elan, Git, Python, and a C toolchain. Run only code you trust: the Lean/Python runner uses your local privileges and is not a sandbox.

Build it by hand ↗Source CI run ↗
LOCAL REPRODUCTION
git clone https://github.com/alok/lean-research-notebook.git
cd lean-research-notebook
git checkout a96aa5e3d5fb03e101aa519eba7bfb74ce7a7d06
lake update
python3 scripts/reproduce.py
python3 -m unittest discover -s tests -v

Generate the full Verso notebook locally, including proof hovers and the complete provenance record.

Context & credits

Directed by Alok Singh; developed with AI assistance. The project extends Verso and adapts its Apache-licensed saved-cell and traversal pattern, originally by David Thrane Christiansen, © 2024–2025 Lean FRO LLC.

Inspired by Microsoft’s Quine announcement, with the NOVA paper as a scientific-tool orchestration precedent. This project has no Quine integration, trained AI, biology data, or efficacy claim. Blueprint, ProofWidgets, and a persistent Lean REPL are future possibilities, not implemented features.

Source snapshot a96aa5e3 · Exact numerical report · Source review