diff --git a/README.md b/README.md
index 18b58418..f5bbb8ef 100644
--- a/README.md
+++ b/README.md
@@ -1,16 +1,30 @@
-# OpenGA
+
Riemannian Geometry Challenge
-A Lean 4 library for geometric analysis.
+In progress.
-## Quick Start
+
+A public, open initiative to build Riemannian geometry into a living,
+machine-verified textbook — a shared foundation anyone can learn from,
+contribute to, reuse, and build on. Made for everyone.
+
-Add the following dependency to your Lean project's `lakefile.lean`:
+
+
+
+
+
+
+
+
+## Use the Lean library
+
+Add the dependency to your `lakefile.lean`:
```
require OpenGALib from git "https://github.com/MathNetwork/OpenGA.git" @ "main"
```
-## Build
+Build:
```
lake exe cache get
@@ -21,13 +35,14 @@ Requires Mathlib at the SHA pinned in `lake-manifest.json`.
## Status
-Pre-`v0.1.0`, experimental. PRE-PAPER `sorry`'d statements and narrow structural axioms are tracked with explicit repair plans in module docstrings (search for `**Sorry status**:` / `axiom`).
+Pre-`v0.1.0`, experimental. PRE-PAPER `sorry`'d statements and narrow structural
+axioms are tracked with explicit repair plans in module docstrings (search for
+`**Sorry status**:` / `axiom`).
## Contributing
-The library is designed for downstream research consumption, teaching use, and Mathlib upstream candidacy. Issues and PRs welcome.
+Issues and PRs welcome.
## License
-OpenGA is released under the Apache 2.0 License.
-See the LICENSE file for details.
+Released under the Apache 2.0 License. See the LICENSE file for details.