lean-ga

A partial formalization of Geometric Algebra (GA) in the Lean formal proof verification system and using its Mathematical Library.

A description of the foundations of this work is published as Formalizing Geometric Algebra in Lean in Advances in Applied Clifford Algebras (note that the web version has been horrendously typeset by the publisher, but the PDF version is readable). The code in this repository has evolved since that publication to keep up with changes to mathlib. We presented an early version of this at ICCA 2020 (slides).

A semi-interactive viewer for the contents of this project can be found at https://pygae.github.io/lean-ga-docs/. Of particular interest are:

• Parts of mathlib contributed as part of this work. These used to live in this repository, but have graduated to mathlib itself. The links below go to the precise version of mathlib lean-ga uses, rather than to the latest mathlib docs.
  • clifford_algebra
    • clifford_algebra_ring.equiv: the real numbers have an isomorphic clifford algebra.
    • clifford_algebra_complex.equiv: the complex numbers have an isomorphic clifford algebra.
    • clifford_algebra_quaternion.equiv: the quaternion numbers have an isomorphic clifford algebra.
    • clifford_algebra.as_exterior: the exterior algebra has an isomorphic clifford algebra
  • exterior_algebra
  • alternating_map
• Translations of other formalizations:
  • geometric_algebra/translations/hol_light.lean
  • geometric_algebra/translations/ida.lean
  • geometric_algebra/translations/laurents.lean
• Additional API on top of the mathlib clifford_algebra:
  • geometric_algebra/from_mathlib/versors.lean, a formalization of versors
  • geometric_algebra/from_mathlib/concrete/cga.lean, a formalization of CGA

To get the full experience of using lean-ga without having to install lean, use the GitPod link at the top of this readme. Wait for the command in the console to finish, then open one of the files referenced above, and wait for compilation to finish (the orange bars to vanish). At this point, you can move the cursor around to view the proof state, and try adding new statements to the file using our definitions.

See this visualization to see which parts of Mathlib are used in this formalization (directly or indirectly).

Update for ICACGA

This repository has been updated to contain some of the examples in the paper "Computing with the universal properties of the Clifford algebra and the even subalgebra", submitted to the ICACGA conference. In turn, that paper contains permalinks that lead back to commits within this repository. Many of the examples in that paper have since graduated to mathlib and are no longer in this repository.

The main results from that work are:

• clifford_algebra.equiv_even: every clifford algebra is isomorphic to the even subalgebra of a larger algebra.
• clifford_algebra.equiv_exterior: every clifford algebra over a ring of characteristic not two is isomorphic as a module to the exterior algebra.

Contributing

We welcome contributions, especially those in the areas outlined in the Future Work section of our paper. In some cases though, your contribution may well be better directed at mathlib itself, especially if it only depends on the parts of our work that have already been integrated into Mathlib.

Project Structure

This project is configured for use with leanproject, and such can be downloaded with leanproject get pygae/lean-ga. The Lean source files can all be found in the src directory, which is structured as follows.

• src/for_mathlib: non-GA formalizations intended for contribution to mathlib
• src/geometric_algebra
  • nursury: various experiments at formalizations approaches
  • translations: partial translations of formalizations in other languages
  • from_mathlib: The core of this formalization, building on top of the clifford_algebra contributed to Mathlib

Additionally, there are some miscellaneous resources in docs/misc, which contain a mixture of links to and excepts from related work, and some initial design ideas and goals.

Naming

There is little precedent for naming third-party Lean libraries; we mirror the choice made by lean-perfectoid-spaces by prefixing the repo name with lean-, and use ga to abbreviate geometric-algebra.