Skip to content
/ lean-ga Public

A partial formalization of Geometric Algebra in the Lean formal proof verification system.

License

Notifications You must be signed in to change notification settings

pygae/lean-ga

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

lean-ga

Gitpod ready-to-code arXiv DOI

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:

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:

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.

About

A partial formalization of Geometric Algebra in the Lean formal proof verification system.

Topics

Resources

License

Stars

Watchers

Forks

Languages