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`: +

+ Powered by Astrolabe +   + Website +   + Join our Discord +

+ +## 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.