Implementation of Gowers & Ganesalingam theorem prover in Lean.
See https://arxiv.org/pdf/1309.4501.pdf for a description. The original implementation in Haskell: https://github.com/EdAyers/Robotone
This repository has been archived by the owner on Aug 30, 2021. It is now read-only.