This repository has been archived by the owner on Aug 30, 2021. It is now read-only.

EdAyers / lean-humanproof Public archive

Notifications You must be signed in to change notification settings
Fork 0
Star 6

Implementation of Gowers & Ganesalingam theorem prover in Lean

6 stars 0 forks Branches Tags Activity

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 14 Commits
_target/deps		_target/deps
src		src
.gitignore		.gitignore
README.md		README.md
leanpkg.path		leanpkg.path
leanpkg.toml		leanpkg.toml

Repository files navigation

lean-humanproof

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

About

Implementation of Gowers & Ganesalingam theorem prover in Lean

Report repository

Releases

No releases published

Packages

No packages published

Contributors 2

Languages

Lean 100.0%