GNC for Lean

A formally verified mathematical library for guidance, navigation and control, using released Lean 4.29.1 and mathlib v4.29.1. It includes Lie groups, mixed-invariant dynamics, preintegration, Magnus algebra, nonlinear control, estimation, reachability and orbital fuel certificates.

Every project .lean file lives under GNC/. import GNC.All exports the complete mathematical development, including all paper applications. The exact-rational CLI is separate in GNC/Tools/. import GNC.Core selects the general mathematics. Individual modules can also be imported. Application proofs live in GNC/Applications/. The manuscripts, reviews, coverage ledgers, experiment programs and their current figures and data live in a separate papers repository that consumes this library as a submodule.

All theorem declarations are checked by Lean's kernel under their stated hypotheses, with no admitted proofs or additional project axioms. The verification contract specifies this claim and its limits. The current verification record identifies the checked source snapshot. This does not claim that every statement in every original paper, numerical simulation or physical vehicle has been completely verified.

Reproduce

nix develop
gnc-cache
lake build
python scripts/verify.py

The flake pins the official Lean compiler, released mathlib and every transitive Lake dependency. No global elan installation or separate mathlib checkout is needed. nix develop materializes pinned sources in .lake/packages and writes the path-based lake-manifest.json. Update dependencies through the flake; do not run lake update.

gnc-cache fetches the released compiled dependency artifacts. After cache setup, the proof build needs no dependency downloads. GNC reuses mathlib's theorems directly. The first setup requires network access and several GB. nix build alone builds the Lean compiler; lake build builds and audits the proof library. The verification command uses Lake's incremental cache and runs the complete axiom audit, source-coverage checks and planner interface checks. Checked project proofs and build traces persist in .lake/build; released dependency artifacts persist under .lake/packages. Lake rebuilds affected modules when sources, imports, build options or the toolchain change. Keep these ignored directories between sessions. An unchanged lake build reuses the checked proofs.

For an explicit clean verification, use nix develop --command python scripts/verify.py --fresh. This rebuilds every project module in an isolated directory and installs the successful build into .lake/build, so subsequent commands reuse it.

nix develop --command python scripts/check_structure.py
nix develop --command python scripts/verify.py --check-report .lake/verification/report.json

The second command checks snapshot correspondence; it does not rerun proofs.

Continuous integration

The library's GitHub Actions workflow runs on pushes, pull requests and manual dispatch. It uses this repository's own flake, fetches the pinned release's mathlib artifacts, and runs the complete verification command above. It then checks that the generated report matches the exact source snapshot and uploads the report and logs, including on failure.

Dependency artifacts and project proof artifacts have separate caches. Lake checks source and import changes before reusing project artifacts; a cache hit does not skip the build or the axiom audit. The workflow pins action revisions and requires no publishing credentials. A hosted CI pass is a separate piece of evidence from a locally generated verification record.

CI saves released artifacts immediately after setup and checkpoints the core proof build before application certificates. It also saves completed project artifacts after ordinary failures, so a retry can resume. An abrupt runner shutdown can prevent final uploads; a saved partial cache is not a passing verification record. GNC_VERIFY_STREAM=1 exposes live Lake output and a minute-by-minute heartbeat while retaining full logs for the final audit. CI also uses GNC_SERIAL_BUILD=1 to run the complete Lake build with one compiler process at a time. This avoids concurrent large certificate checks; it does not skip any module or relax the verification policy. The same override can be used locally on machines with limited memory.

Applications and papers

Notable results and limits are described in the library overview, and the application index links each proof aggregate. The library design explains the separation between general mathematics and applications and the proposed mathlib contribution plan.

The manuscripts, adversarial reviews, coverage ledgers and experiment programs live in a separate papers repository that includes this library as a submodule and builds the documents and numerical experiments against these proofs.

Repository layout

• GNC/: every project Lean source; general mathematics, applications and verification tooling.
• docs/: library design and the current verification record.
• scripts/: Python setup, verification and repository checks.
• nix/, flake.nix, flake.lock: reproducible environment and Lean toolchain.

.lake/, .direnv/, Python caches and Nix result* links are ignored. Nix output links point to /nix/store; they are build artifacts, not source files. Keep new output links under .lake/, or pass --no-link.

License

GNC for Lean is licensed under the Apache License, Version 2.0. See LICENSE and NOTICE for details. Copyright 2026 CogniPilot Foundation.

The library reuses mathlib, which is also distributed under the Apache License, Version 2.0, as a dependency.