You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
Shad Amethyst ee3cdfe13b
:up_arrow: Upgrade mathlib
11 months ago
Rubin :up_arrow: Upgrade mathlib 11 months ago
old Remove namespace that conflicted with #aligns 1 year ago
.gitignore Raw port through mathport 1 year ago
README.md 💩 Messy draft code to work towards the end of the proof 12 months ago
Rubin.lean :up_arrow: Upgrade mathlib 11 months ago
lake-manifest.json :up_arrow: Upgrade mathlib 11 months ago
lakefile.lean Raw port through mathport 1 year ago
lean-toolchain :up_arrow: Upgrade mathlib 11 months ago

README.md

Lean4 port of the proof of Rubin's Theorem

THis repository contains a (WIP) computer proof of Rubin's Theorem, which states that if a group acts on two topological spaces while satisfying enough conditions, then there exists a homeomorphism between those two topological spaces, such that the homeomorphism preserves the group structure of the group action.

It is based on "A short proof of Rubin's Theorem" (James Belk, Luke Elliott and Franceso Matucci), and a good part of the computer proof was written in Lean 3 by Laurent Bartholdi.

The eventual goal of this computer proof is to have it land into Mathlib.

Installation and running

You will need an installation of elan and git.

Then, simply run the following:

# Clone this repository
git clone https://github.com/adri326/rubin-lean4

# Navigate to the folder created by git
cd rubin-lean4

# This will download mathlib, and try to download a set of pre-compiled .olean files,
# so you won't have to re-compile the entirety of mathlib again (which takes a good hour or two)
lake exe cache get

# Build the code (if no errors are printed then Lean was happy)
lake build