Abstract algebra provides a large hierarchy of properties that a collection of objects can satisfy, such as forming an abelian group or a semiring. These classifications can arranged into a broad and typically acyclic directed graph. This graph perspective encodes naturally in the typeclass system of theorem provers such as Lean, where nodes can be represented as structures (or records) containing the requisite axioms. This design inevitably needs some form of multiple inheritance; a ring is both a semiring and an abelian group.

In the presence of dependently-typed typeclasses that themselves consume typeclasses as type-parameters, such as a vector space typeclass which assumes the presence of an existing additive structure, the implementation details of structure multiple inheritance matter. The type of the outer typeclass is influenced by the path taken to resolve the typeclasses it consumes. Unless all possible paths are considered judgmentally equal, this is a recipe for disaster.

This paper provides a concrete explanation of how these situations arise (reduced from real examples in mathlib), compares implementation approaches for multiple inheritance by whether judgmental equality is preserved, and outlines solutions (notably: kernel support for η-reduction of structures) to the problems discovered.

Typically, Geometric Algebra (GA) is introduced via choosing an orthogonal basis, and defining how multiplication acts on this basis according to some simple rules. This works well computationally, but can obscure insight mathematically. In particular, operations defined in terms of coordinates on a multivector basis can be difficult to rigorously show to be “coordinate-free”, especially in large algebras. This paper explores the use of the “universal property” to ensure that operations are “coordinate-free” by construction. To build some insight for applying the universal property, we draw parallels to the process of writing recursive programs. We then demonstrate a novel result using this approach by deriving a universal property of the even subalgebra. Armed with this second universal property, we provide an explicit construction for a well-known equivalence between any Clifford algebra and its “one-up” even subalgebra. We conclude with some remarks about formalization of these ideas in a theorem prover.

In principle, dependent type theory should provide an ideal foundation for formalizing graded rings, where each grade can be of a different type. However, the power of these foundations leaves a plethora of choices for how to proceed with such a formalization. This paper explores various different approaches to how formalization could proceed, and then demonstrates precisely how the authors formalized graded algebras in Lean’s {\mathlib}. Notably, we show how this formalization was used as an API; allowing us to formalize graded structures such as those on tuples, free monoids, tensor algebras, and Clifford algebras.

Working with noncommutative algebras in computer algebra systems (CAS) can be challenging. Taking a popular CAS as an example; Python’s sympy can run into various difficulties when working with the matrix and quaternion algebras, and building more unusual algebras only makes matters worse. While on the surface solving a similar class of problems to CAS, theorem provers offer a very strong correctness guarantee. As it turns out, the design decisions that ensure this guarantee are the same as those which provide the extensionality needed for adding new algebraic constructions. With this background, this talk acts as an introduction to the Lean theorem prover by example, and demonstrates some of the trade-offs to be made by choosing to use a theorem prover over a CAS. With the help of Lean’s comprehensive library of formalized mathematics, Mathlib, I’ll show how to manipulate and simplify some matrix expressions. Lean and Mathlib are a collaborative effort; this talk concludes with a summary of the more interesting parts I myself have contributed.

This paper explores formalizing Geometric (or Clifford) algebras into the Lean 3 theorem prover, building upon the substantial body of work that is the Lean mathematics library, mathlib. As we use Lean source code to demonstrate many of our ideas, we include a brief introduction to the Lean language targeted at a reader with no prior experience with Lean or theorem provers in general. We formalize the multivectors as the quotient of the tensor algebra by a suitable relation, which provides the ring structure automatically, then go on to establish the universal property of the Clifford algebra. We show that this is quite different to the approach taken by existing formalizations of Geometric algebra in other theorem provers; most notably, our approach does not require a choice of basis. We go on to show how operations and structure such as involutions, versors, and the Z2-grading can be defined using the universal property alone, and how to recover an induction principle from the universal property suitable for proving statements about these definitions. We outline the steps needed to formalize the wedge product and N-grading, and some of the gaps in mathlib that currently make this challenging.

Scalar actions are ubiquitous in mathematics, and therefore it is valuable to be able to write them succinctly when formalizing. In this paper we explore how Lean 3’s typeclasses are used by mathlib for scalar actions with examples, illustrate some of the problems which come up when using them such as compatibility of actions and non-definitionally-equal diamonds, and note how these problems can be solved. We outline where more work is needed in mathlib in this area.

This report documents the current state of, and latest work done towards, an evolving multidisciplinary project that has been passed down through more than 10 years of students within the Cambridge University Engineering Department. The core theme of this ongoing work is to produce a self-balancing rider-less unicycle.

In this iteration of the work, the focus is on a smaller unicycle, and producing an affine controller capable of balancing it via a machine-learning route, rather than by forming a detailed model and applying control theory. This involves applying a technique known as Pilco, for which a Matlab toolbox exists, maintained by the department. This toolbox has already been shown to be successful when applied to a simulation of a large unicycle.

The small unicycle was the subject of a very similar project last year, in which some electrical and mechanical problems were identified and fixed, and many learning experiments were performed, with limited success. A number of outstanding issues were raised, from which this work addresses: automating the transfer of data to and from the robot, dealing with initial orientations by using data from the accelerometer, and building a more representative unicycle model in simulation.

Numerous new problems were found in the existing software and electronics during attempts to replicate previous experiments. Since many of these corresponded to misunderstanding the representation of orientation in 3D, an appendix is included that summarizes these ideas. Rather than continuing to use these slow full-system experiments to expose problems, this work focussed more on an approach of critically reviewing source code, and performing simple hardware tests. Code review revealed many hard-to-decipher pieces of code, for which new abstractions were written to ease their readability, applying modern software engineering principles – often exposing bugs in the process. Overall, large amounts of software was rewritten, which represented the bulk of the work on this project. Minor improvements were also made to the human interfaces to the software, both graphical and logical in nature – greatly improving its transparency, enabling problems to be more easily identified.

Simulations were performed to evaluate a claim made that a \17° roll restriction was impairing learning progress. This was shown to be true, but a simple solution of adding a cost function term was proposed and tested that diminished this effect in simulation, without incurring a mechanical redesign. Despite this, learning efforts on the hardware were even less successful than before, and did not meet the expectations set by simulations.

In outlining future work for this project, it is noted that the Pilco framework would benefit from the application of Automatic Differentiation, possibly necessitating a programming language change. It is also discussed that an affine controller is unlikely to ever be satisfactory, with a quadratic controller shown to be desirable by means of a thought experiment. Finally, observations are made that the state constraints need to be integrated into the prediction process to avoid underestimating loss.

The full text of this report in PDF format (complete with hyperlinks), selected raw data used within, and links to all the source code used, will be made available online at \url{https://github.com/eric-wieser/masters-thesis/releases}.