From 6fb88fd2f44cb1ff83663f0fee9c5ec04a6b4129 Mon Sep 17 00:00:00 2001
From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com>
Date: Wed, 27 May 2026 00:26:47 -0400
Subject: [PATCH] docs(readme): sync with spec-only main

---
 README.md | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

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`).