A Lean 4 library for geometric analysis.
Add the following dependency to your Lean project's lakefile.lean:
require OpenGALib from git "https://github.com/MathNetwork/OpenGA.git" @ "main"
lake exe cache get
lake build
Requires Mathlib at the SHA pinned in lake-manifest.json.
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).
The library is designed for downstream research consumption, teaching use, and Mathlib upstream candidacy. Issues and PRs welcome.
OpenGA is released under the Apache 2.0 License. See the LICENSE file for details.