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
|
11 months ago | |
---|---|---|
Rubin | 11 months ago | |
old | 1 year ago | |
.gitignore | 1 year ago | |
README.md | 12 months ago | |
Rubin.lean | 11 months ago | |
lake-manifest.json | 11 months ago | |
lakefile.lean | 1 year ago | |
lean-toolchain | 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