# Lean projects

While much Lean development takes place in the mathlib repository, there are many other projects using Lean that are developed and maintained by members of the community. We list here a selection. Many of these projects are designed to be imported as dependencies in other developments. At the bottom of this page, you can see a summary of which projects are compatible with which Lean versions. If two projects both support the same Lean version, you can likely use them together.

To add a project to this list, please see the directions at the leanprover-contrib repository.

This list and the repository that manages it are both works in progress. Please add your own project and report any problems in that repository.

##### lean-perfectoid-spaces
###### maintained by @kbuzzard@jcommelin@PatrickMassot

Perfectoid spaces are sophisticated objects in arithmetic geometry introduced by Peter Scholze in 2012. We formalised enough definitions and theorems in topology, algebra and geometry to define perfectoid spaces in Lean. See also our project webpage and paper.

##### lftcm2020
###### maintained by @jcommelin@PatrickMassot

This repository contains tutorials about Lean and mathlib that were developed for the workshop Lean for the Curious Mathematician, held in July 2020. The tutorials range from introductory lessons on numbers, logic, and sets to advanced lessons on category theory and manifolds. In addition to the materials found in this repository, we recommend watching the videos of the tutorials and lectures from the workshop.

##### topos
###### maintained by @b-mehta

This repository contains formal verifications of results in Topos Theory, drawing from "Sheaves in Geometry and Logic" and "Sketches of an Elephant". It currently includes a range of constructions and theorems about both Grothendieck topoi and elementary toposes.

##### sudoku
###### maintained by @TwoFx

This is an implementation of sudoku, written in Lean. When you open a level in VS Code, a sudoku board is displayed in the goal view. You can put numbers (and also pencil marks) on the board by adding hypotheses, but you have to prove that the placement of the number follows logically from what is already on the board! There are some tactics to help you with this, and you can also prove theorems to build up your personal library of sudoku theory.

##### mathematica
###### maintained by @robertylewis@minchaowu

Connects Lean to the computer algebra system Mathematica. This project offers a bi-directional translation between the two systems. From within Lean, you can evaluate Mathematica commands, possibly including translated Lean expressions, and process the results. From Mathematica, you can access a Lean environment.

Examples of calling Mathematica from Lean can be found at robertylewis/mathematica_examples, and examples in the other direction at minchaowu/mm-lean. These repositories are not in the contrib list because they depend on Mathematica, which is proprietary software. See also our project webpage with a link to our paper about this project.

##### super
###### maintained by @gebner

Version one of a small superposition prover written in Lean. This repository introduces a tactic super which attempts to solve problems in first order logic, possibly given a list of extra hypotheses.

This version is not compatible with community releases of Lean.

##### rubiks-cube-group
###### maintained by @kendfrey

This project formalizes the Rubik's cube group as a product of corner orientation, corner permutation, edge orientation, and edge permutation.

The solvable subgroup is defined as the the set of positions where both orientations sum to 0 and the permutations have the same sign.

This project includes a widget to visualize elements of the group as physical puzzle states.

##### super2
###### maintained by @gebner

Version two of a small superposition prover written in Lean. This repository introduces a tactic super which attempts to solve problems in first order logic, possibly given a list of extra hypotheses.

## Projects by supported Lean versions

If you want to import multiple projects in your own, you should choose a Lean version that is supported by each of these dependencies.

• A ✓ in the x.y.z column means that the project has a lean-x.y.z branch, all of its dependencies have lean-x.y.z branches, and the project builds successfully using the most recent commits on all of these lean-x.y.z branches.
• An × in the x.y.z column means that the project has an lean-x.y.z branch but it fails to build.
• No mark in the x.y.z column means that the project does not have an x.y.z branch.

Note that an × does not necessarily mean the project does not compile, just that it does not compile with updated dependencies.