diff --git a/README.md b/README.md
index bd2d426..3dbb7be 100644
--- a/README.md
+++ b/README.md
@@ -2,23 +2,21 @@
 
 A Lean 4 library that turns formal proofs into computable mathematical objects.
 
-[Documentation](https://proof-atlas.vercel.app/) · [White Paper](whitepaper/) · [Contributing](CONTRIBUTING.md)
+[White Paper](whitepaper/) · [Contributing](CONTRIBUTING.md)
 
-## Quick start
+## Status
+
+Main branch contains the design specification for the proof
+hypergraph. Implementation is on the `development` branch and
+will be promoted here as it reaches production quality.
+
+## Build
 
 ```bash
 cd lean
-lake exe cache get
 lake build
 ```
 
-```lean
-import ProofAtlas
-
-#atlas.resistance Nat.add_zero Nat.add_comm
-#atlas.graph Nat.add_zero
-```
-
 ## License
 
 Apache 2.0 (see `LICENSE`).