Human-Oriented-ATP
Popular repositories Loading
-
-
automatic-proof-generalization
automatic-proof-generalization PublicA Lean tactic (`autogeneralize`) which takes in a proof and generalizes it 'as far as the proof allows.'
Lean 7
-
-
lean-humanproof
lean-humanproof PublicAn implementation of a proof environment in Lean for formalizing motivated proofs, based on Ed Ayers' thesis: https://www.edayers.com/thesis.
Lean 2
-
motivated-proof-facilitator
motivated-proof-facilitator PublicA graphical interface that makes it convenient to construct "motivated proofs" through a series of point-and-click moves.
-
Repositories
- automatic-proof-generalization Public
A Lean tactic (`autogeneralize`) which takes in a proof and generalizes it 'as far as the proof allows.'
- motivated-proof-facilitator Public
A graphical interface that makes it convenient to construct "motivated proofs" through a series of point-and-click moves.
- lean-humanproof Public
An implementation of a proof environment in Lean for formalizing motivated proofs, based on Ed Ayers' thesis: https://www.edayers.com/thesis.
- LeanGeom Public
- lean-tactics Public
- motivated-proof-interface Public Forked from leanprover-community/lean4web
A point-and-click interface for constructing motivated proofs.
- proof-specimen Public
- tree-rewriting-game Public
People
This organization has no public members. You must be a member to see who’s a part of this organization.
Top languages
Loading…
Most used topics
Loading…